So, for my UROP project at Imperial, I had to formalize problems from Math contests in Lean. Of course, I really derailed and tried to prove some other things, too, but still. My most recent accomplishment is the formalization of the second problem from the Balkan Math Olympiad 2019. To be fair, I completely forgot about the BMO up until I scrolled through an old Romanian Mathematical Gazette that I had laying around. I read the article in the Gazette about the competition, and, after looking over the solutions, I had an epiphany: I could teach my laptop how to solve them! Being more-or-less familiar with inequalities, I decided to look over the second problem. Here it is:
Let \(a, b, c \in \mathbb{R}\) such that \(0 \leq a \leq b \leq c\) and \(a + b + c = ab+bc+ca \ge 0\). Prove that \(\sqrt{bc}(a+1)\geq 2 \).
Proof: The Gazette showed the solutions that the students gave, and the following is Dragos Crisan's proof. Let \(t = \sqrt{bc}\). If \(a \geq 1\), then both \(b\) and \(c\) will also be bigger than 1, and the problem is trivial.
If \(a \le 1\), then we can write \(t^2 = bc = a + (1-a)(b+c) \geq a + 2(1-a)t\), where the inequality is due to AM-GM. Thus, we have obtained the fact that \(t^2 - 2(a-1)t-a \geq 0\). From here on, Dragos looks at the roots of the function \(f(x)=x^2-2(1-a)x-a\). A quick calculation with the discriminant shows that the roots are \(x_2 \leq 0 \leq x_1\).
By observing that \(f(\frac{2}{a+1})=\frac{-a(a-1)^2}{(a+1)^2} \leq 0\), we can deduce that \(\frac{2}{a+1}\) is between the roots. Similarly, since \(f(t) \geq 0\) and \(t \geq 0\), we deduce that \(t \geq x_1 \geq \frac{2}{a+1}\). Multiplying by \(a+1\), we get the conclusion that \(\sqrt{bc}(a+1)\geq 2 \). ⬜
This proof is really clever and short, which adds to its beauty. To us, it seems easily understandable, so I wondered if my laptop would think the same. When I started writing it down, I wasn't sure if it was going to understand it, but apparently it did. \(\href{https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fgist.githubusercontent.com%2FSoccolo%2F869caf89d5a9a29864d899791d02b634%2Fraw%2Fd00813da7e9d9ce2ec07329c84a8e546714532ec%2FBalkanMOP2.lean}{Here}\) it is. The online editor is pretty slow; if you want the real deal, feel free to download Lean. Also, in a few months, the code may not work anymore; Lean is constantly getting updated, and some inefficient tactics may be deleted.
You may have noticed in the proof that I ignored some aspects, such as why one root is negative and one is positive, or the calculation of \(f (\frac{2}{a+1})\) and so on. This can't happen with computers, they are a lie detector when it comes to proofs. I even had to prove that \(\sqrt{4}=2\), although it is very probable that there was a one-liner that could have solved that problem. I am new to Lean myself, so the code isn't as good as it should be; the problem could be solved more efficiently. Lean uses something called 'Calculus of Constructions', which basically means that it deals with combining propositions and proofs in order to get something. Each statement to the right, e.g, let's say, 'obs', is actually a proof of whatever it mentions. For instance, if the half-screen on the right, which is called the 'pretty printer' says something about 'obs:\(4=2*2\)', it means that it has a proof that \(4=2*2\). Using different commands and lemmas from the library (e.g the things that I imported in the beginning), the computer does what we did above, but way more rigorously. This is an advantage of computers: they can't be wrong unless we give them wrong info. Since Lean is built on the axioms of Mathematics, such as the Peano Axioms, it can't be wrong.
On the topic of axioms, here's something interesting. I was formalizing the first problem from the same competition, something about prime numbers, and I wanted to prove that \(2^n-n^2 \geq 0\), for all natural numbers. Normally, I would have done it with induction, but Lean thought it was obvious. Surprised, I checked why it thought that, because it didn't seem obvious to me. Here comes the computer's understanding of axioms: I was working with the natural numbers, where Peano rules. Since I was only using commands and libraries attributed to the natural numbers, Lean only used those axioms, so integers, reals, etc didn't exist for it at that moment! Since Peano stated that \(0 \neq a + 1\), for any \(a \in \mathbb{N}\), Lean considered that 0 is the smallest number, and anything that should normally be smaller than 0 is actually 0, which is axiomatically correct, but intuitively wrong for us. Fortunately, this doesn't lead to wrong results: you can't prove that \(0 \leq 1-2 \to 2 \leq 1\), because Lean understands that it's wrong.
Another cool fact: Lean actually caught me when I was wrong! I was proving the Heisenberg Uncertainty Principle from Quantum Mechanics in Lean, and, instead of using the complex inner product, I used the real inner product, and I eventually proved something obvious, that describes Classical Mechanics. Lean isn't made for formalizing Physics, but Quantum Mechanics is very mathematical in nature, and if you only deal with the Mathematical Physics part, it's pretty doable.
In the future, maybe 10-20 years from now, computers may become assistants or actual theorem provers, proving theorems that we can't right now. But, at the moment, they are in need of our help, just like children that are taught Maths. However, the student of today is the teacher of tomorrow, so let's tutor them!
This was it for today folks! Tune in next time for some Mathematical Physics (aka my newest burning hobby; already done courses in Quantum Mechanics and Special Relativity, also reading 'Foundations of Mathematical Physics' by Sadri Hassani, great book), some Lean, or something completely random!
Cris.
