Can my computer understand more Maths than me - The Imperial College Mathematics Competition

 

Hey folks, long time no see. Life has been pretty busy in the past few months, hasn't it? In order to make life easier for Math students across the UK, several students at Imperial, myself included, ran the 4th edition of the \(\href{https://icmathscomp.org/}{Imperial \ Mathematics \ Competition}\). This year, we went for an online format, kinda like the IMC last summer. Overall, we had an impressive amount of people attending the first round; over 120 students participated at the first round, the top 50 qualifying for the second one.

All problems were exciting and fun, the organizing team was excellent, and it was great working with likeminded individuals. In this post, I'll go over one of the two problems that I proposed: the 3rd problem from the second round. I thought of this problem while working on some integral inequalities. Here it is:

Let \(f,g,h\) be continuous functions and \(X\) a random variable such that \(E(g(X)h(X))=0\) and \(E(g(X)^2) \neq 0 \neq E(h(X)^2)\). Prove that \(E(f^2(X))-\frac{E^2(f(X)h(X))}{E(h^2(X))} \geq \frac{E^2(f(X)g(X))}{E(g^2(X))}\).

Solution: What do expected values and integrals have in common? Well, sure, expected values are integrals, but there is another thing; both can be written as inner products. For instance, \(<f , g> =\int_{0}^{2\pi} f(x) g(x) dx\) is an inner product. Similarly, one can think of \(E(XY)\) as an inner product between two vectors, which in this case are random variables, or functions thereof. Thus, this problem is actually linear algebra in disguise!

Let's rewrite it using only linear algebra. We now have to prove that, if \(f, g, h\) are vectors on a vector space over \(\mathbb{R}\) such that \(<g, h>=0\), \(<g,g> \neq 0 \neq <h,h>\), the following inequality holds:

\(\begin{equation} ||f||^2 \geq \frac{(f,g)^2}{||g||^2} + \frac{(f,h)^2}{||h||^2} \end{equation} \)

For any \(\lambda \in \mathbb{R}\), we have \(\lambda (f,g)= (g,h+\lambda f) \leq ||g|| \cdot ||h+\lambda f||\), by Cauchy. Squaring, we obtain that \(\lambda^2 (f,g)^2 \leq ||g||^2 \cdot ||h+\lambda f||^2\). Now dividing by \(||g||^2 \neq 0\) yields \[\lambda^2 \frac{(f,g)^2}{||g||^2} \leq ||h+\lambda f||^2 = ||h||^2 + 2 \lambda (f,h) + \lambda^2 ||f||^2.\] We can take everything on the right side, to obtain that 

\(\begin{equation} \lambda^2 (||f||^2 - \frac{(f,g)^2}{||g||^2}) + 2 \lambda (f,h) + ||h||^2 \geq 0,\end{equation}\)

for all \(\lambda \in \mathbb R\). We consider this a quadratic equation in \(\lambda\), and use the fact that, for the equation to always be positive, we need the discriminant to be smaller or equal to 0. We conclude that \(||f||^2-\frac{(f,h)^2}{||h||^2} \geq \frac{(f,g)^2}{||g||^2}\), which solves the problem. 

This was fun, right? The inequality stated works for any inner product space; I could have written integrals, or the dot product, or anything that came to mind. Thus, the solution is as general as possible. You know who else likes generalisations? My old buddy Lean. 

I wrote inner products and the Cauchy inequality from scratch; they were already written in Lean's library in a much more efficient way than I could have come up with, but I felt that proving all that I needed myself would be a better exercise. \(\href{https://gist.github.com/Soccolo/0ca77b63d90556dc94897e65845439a8}{Here}\) is the code.

In the beginning, I defined what an inner product is; you may observe that it is the real inner product, as I haven't thought about making the inequality more general. I also proved some properties of inner products; the function \(f\) is a general inner product, so any result about it is a result about the inner products I defined. Cauchy-Schwarz was pretty interesting to prove; I am certain that there is a way easier way of proving it, but I am still a Lean novice. After Cauchy-Schwarz, we delve immediately into the problem at hand; we prove some lemmas and small results, and compile them together in a neat way to get a proof.

Every 'have ...' is some sort of lemma inside a proof. The logic is the classical 'divide and conquer' idea; I split the problem into pieces, then glued them together to get a result. Lean treats each such lemma inside the proof as a proof itself; when you use a result in Lean, you don't quote the result, you actually use a proof of the result. Thus, through each 'have ...', I got lots of results that I used in order to prove the Cauchy inequality and the contest inequality. I am not the best person to explain how Lean works, so why don't you check out the community's \( \href {https://leanprover-community.github.io/}{website}\)?

It's a fun time to be alive if you're a Mathematician. Lean 4 has been released and it's still being worked on, the Maths community is more intertwined than ever, the quantum world is unravelling before our eyes, big data is beginning to play a huge role in the world's affairs. Tune in next time for another dive into what Maths has to offer, or something completely random!

Cris.

What if my laptop could beat me at the Balkan Math Olympiad?

Hey there folks, Cris here, showing you another random Mathematics-related thing that I have recently done!

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.