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.

The Experience of the First Online International Mathematics Competition for University Students

Hi there folks! Long time no see! Lots of things happened ever since the last article: I took my exams, summer holiday started, and the first online International Mathematics Competition for University Students took place. It has been a long-while dream of mine to take part in this competition, and I was hell-bent on participating this year. Turns out, however, that I didn't get to participate the way I wanted; due to the Covid-19 pandemic, it was held online.

As a teamless student, I was supervised by Ivan the Confessor, alongside many other teamless students, on a Google Meet call. We had several possible timezones in which we could take the contest: the European timezone, which was from 7 AM UTC to 11 AM UTC, the Asian timezone, from 2 AM UTC to 6 AM UTC, and the American timezone, from 2 PM UTC to 6 PM UTC. Of course, as the chad I am, I woke up at 2 AM UTC aka 5 AM Romanian time and solved the problems then. Just kidding, I took the contest in the European timezone. My computer's camera crashed, and I had to shut it down and use the phone in order to record myself and my desk instead. 

Since the Olympiads ended for me in the 12th grade, I forgot how it felt to actually be in a contest, especially an international one. So, as the contest began, I was incredibly scared. Fortunately, this fear always passes when the subjects come. One important thing to note about me: I cough whenever I'm nervous. It's not a very quiet cough, but an incredibly loud one, with sound waves travelling through all 11 dimensions of M-string theory and beyond. My cough is literally Covid-20. This time, however, I didn't feel the need to cough, which was pretty odd. 

After printing the subjects, I swiftly started working on them. I solved the second problem first, since it was a matrix problem; it couldn't have taken me more than 10 minutes. The problem is as follows:

Let \(A, B \in M_n(\mathbb{R})\) such that \(rk(AB-BA+I)=1\). Prove that \(Tr(ABAB)-Tr(A^2B^2)=\frac{1}{2}n(n-1)\).

Solution: It is a pretty known fact that, if \(A \in M_n(\mathbb{R})\) is a matrix of rank \(r\), then there exist matrices \(E \in M_{n,r}(\mathbb{R})\) and \(F \in M_{r,n}(\mathbb{R})\) such that \(A=EF\). In this case, these matrices were vectors, so \(A^2=EFEF=E(FE)F\), where \(FE\) is a real number due to matrix multiplication. Since \(FE=Tr(FE)=Tr(A)\), we get that \(A^2=Tr(A)A\), which characterizes all matrices of rank 1. Let us apply that in our problem. 

By squaring, we get that 

\((AB-BA+I)^2=\)

\(Tr(AB-BA+I)(AB-BA+I)\), which is equal to \(n(AB-BA+I)\). If we apply trace again, and equalize the traces in \((AB-BA+I)^2\), we get the conclusion. 

The problem wasn't too hard, but it required a trick. Another possible way of doing it would have been with the Jordan canonical form, but it revolved around the same trace idea. 

The first problem of the contest wasn't my cup of tea. It was combinatorics, and I'm not trained in it. It took me about an hour and hour and 45 minutes to finally catch on to it, after failing miserably at calculations that shouldn't have been too hard. Here's the problem:

Let \(n \in \mathbb{N}^*\). Compute the number of words \(w\) that satisfy all the following properties: 

(1): \(w\) consists of \(n\) letters, all of them from the alphabet {a,b,c,d}.

(2): \(w\) has an even number of a-s

(3): \(w\) has an even number of b-s

Solution: First, let us observe that the total number of words is \(4^{n}\), for a certain \(n\). Consider the following sequences: 

\(a_n\) = number of n-words containing an odd number of both a and b;

\(b_n\) = number of n-words containing an odd number of a or an odd number of b, but not an odd number of both;

\(G_n\) = number of n-words containing an even number of both a and b, e.g 'good' words.

Thus, \(a_n+b_n+G_n=4^n\). Now, let's find a recurrence. We can obtain a word with a or b odd, but not both odd, by adding a c or a d to a word with only one odd, an a or a b to a word with both odd, and an a or a b to a good word. Thus, \(b_{n+1}=2(a_n+b_n+G_n)=2 \cdot 4^{n}=2^{2n+1}\).

By a similar argument, \(G_{n+1}=b_n+2G_n\), so we have that \(G_{n+1}-2G_n=2^{2n-1}\). After solving the recurrence, we obtain that \(G_n=4^{n-1}+2^{n-1}\). Of course, I couldn't observe this without making calculation mistakes; still, I eventually solved the problem correctly. 

After solving these 2 problems, I looked over problem 3. Seeing that I couldn't read it, I skipped over to problem 4. Problem 4 was a result about polynomials, and it was solvable, if you knew enough Complex Analysis and had the brilliance to figure out that it was a Complex Analysis problem. I didn't have that brilliance. 

I was pretty pleased with myself for proving 2 of the 4 problems, and I was already envisioning myself winning a first prize. Then, second day came, with 4 new problems for me to attempt. I solved the first one in the first 45 minutes of the contest, and then struggled for the rest of the contest on the second one. Here's the proof that I gave for the first problem:

Find all \(f:\mathbb{R}\to (0,\infty)\) twice differentiable functions such that \(f ''(x)f(x)\geq 2(f '(x))^2\).

Solution: One first observation is that \(f\) is convex. Indeed, since \(f\) and \((f '(x)^2\) are both positive, \(f ''(x)\) is also positive. 

The second observation is the one that took me the most of those 45 minutes. Let's look at \(\frac{1}{f}\). Observe that its second derivative is exactly \(2(f'(x))^2-f''(x)f(x)\leq 0\), so \(\frac{1}{f}\) is concave. It is a known fact that the only strictly positive concave functions are constant ones, so \(\frac{1}{f}\) is constant, and \(f\) is, thus, a positive constant. During the contest, I said that the only functions satisfying \(f\) convex and strictly positive and \(\frac{1}{f}\) concave are constant ones, but I discussed the fact poorly; thus, I lost one point. More on that later. 

Next, for the following 3 hours, I tried solving problem 2. Problem 2 went as follows:

Find all prime numbers \(p\) such that there is only one \(a \in \{1, 2, ... p\} \) such that \(p | a^3-3a+1\). 

Solution: For the rest of the proof, we shall work in \(\mathbb{Z_p}\).  I wanted to prove that, if the equation has a solution, there must also be another one, a function of \(a\). Here's the trick: see that, if \(a\) is a solution, \(a^2-2\) is also a solution. One can also check that \(-a^2-a+2\) is a solution. How could you possibly see these solutions? By looking at the solutions of \(X^3-3X+1\), which you could find through Cardano's formula. By solving the resulting equations, it could be seen that \(p=3\) is the only solution.

Another possible solution, one that one of my friends found, was by working with grade two equations in \(\mathbb{Z_p}\) and discriminants. Another one thought of using a trick found in an old IMO, that said that, if such p exists, then it's of the form \(9k+1\) or \(9k-1\). This trick used field extensions, which were used in one of the official solutions. Problem 3 of the second day was something about groups, which actually looked doable, but I spent all of my time on problem 2, hoping that it was a trick that I'd figure out. 

After the time was up, I scanned the solutions and uploaded them in a Dropbox. Funny story: after the first day, I sent an email, asking if my problems were sent. An organizer replied that they were sent, but that, on problem 3's solution, I only wrote the number of the problem. To that, I replied: 'Yup, it's intentional.' XD

The results started coming the next day. The people at IMC were uploading results problem by problem, and they started uploading them at 2 am Romanian time. One of my friends and I waited for the results for a while. They stopped uploading results at 3:15 am. I kept waiting until 4 am. They resumed uploading results in the morning, and finished at 12:00 Romanian time. The next day, they also announced the prizes. I got 29 points, and a second prize; firsts were given to those with 30 or more. So, because of that faulty explanation, I lost the point that would have gotten me a first. You have no idea how annoyed I was when I saw that XD

Overall, this IMC was a pretty pleasant experience. I haven't prepared too much for it, so life has done me justice; getting a gold medal, the same prize as many people that have been preparing for the whole year, would have been unfair. I'll definitely be participating at next year's IMC, which will hopefully take place IRL, in Blagoevgrad, as it should have taken place this year. Hope that 1 point won't meme me again. 

Before I end this article, I want to announce something: I'm writing a Maths problem book! It will contain problems highlighting interesting techniques and ideas, and it will probably be open access. The book could be used as preparation material for Student Competitions or Romanian Olympiads. I'll probably release an early access version in October, after adding more problems. At the time of speaking, the book has 40 pages with fully solved problems. It includes chapters on Algebra, Analysis, Applied Mathematics, and, something that I've picked up only recently, Formal Theorem Proving! For the last one, I'm using a Proof Assistant Program called Lean. The book will contain problems that I haven't added on this blog, such as the following: 

Anyway, it's time to end this post. Tune in next time for some Algebra, Complex Analysis, Mathematical Physics, my thoughts on stuff, or something completely random!

Cris.