How easy it is to admire a work of art, but how difficult it is to create it! Artistic creation is similar to mathematical creation. We can all appreciate Euclid’s proof of the infinity of primes, but most feel incapable of generating a mathematical proof. Some will admire classical music, others rock music, some prefer the paintings of Velázquez, others Kandinsky, some theatre, others cinema. There will be no one who does not recognise that some artistic manifestation moves them. But how difficult it is to be an artist. To get rid of the responsibility of not being creative, we invoke genius.
Difficult to find but easy to admire.
Today we comment not on a mathematical publication but on a milestone in the practice of mathematics. On the 5th of this month of June, for the first time in history, a mathematician, Peter Scholze, has verified his proof of a difficult theorem by means of a computer, later on we will explain its connection with my previous comments on artistic and mathematical creation.
Doubts in Mathematics
Mathematics are expected to be a clear and crisp terrain. Two and two make four, unquestionably. But this, which is true in general, is not without its nuances. Situations of confusion have often arisen. Abel, the Norwegian mathematician, had to bring order to the study of infinite series, in which case the lack of precise definitions had led to confusion. The Italian school of algebraic geometry which flourished between 1835 and 1935, with prestigious names such as Enriques, Severi and Castelnuovo, ended up accepting non-rigorous principles which led to contradictory results. Modern algebraic geometry, led by Grothendieck, put an end to this situation by achieving a completely rigorous treatment of the subject.
The endeavour of axiomatisation of mathematics in the 20th century seemed to have put an end to these problems, which were often due to imprecise definitions. But another major problem has arisen, and that is complexity. There are many examples, but I will choose one to explain the current situation. The classification theorem for finite simple groups. These groups are like the components of any finite group. The proof of the theorem that describes them all one by one consists of tens of thousands of pages, spread over hundreds of journals, written by hundreds of mathematicians and published between 1995 and 2004. Gorenstein and others are trying to write a unified proof, have published nine volumes and expect to need at least another five. With such complicated proofs it is not surprising that doubts arise about their validity.
There are extreme cases such as the Busemann-Petty problem and its (double) solution by Gaoyong Zhang. This mathematician has published two papers in the best mathematical journal:
[1] Zhang, Gaoyong, Intersection bodies and the Busemann-Petty inequalities in \(\textbf{R}^4\), Ann. of Math. 140 (1994) 331–346.
[2] Zhang, Gaoyong, A positive solution to the Busemann-Petty problem in \(\textbf{R}^4\), Ann. of Math. 149 (1999) 535–543.
In [1] Zhang proves that the solution to the Busemann-Petty problem is negative in \(\textbf{R}^4\). In [2] he proves that just the opposite is true. A case in which the reviewer took an incorrect reasoning for granted. But anyone who understands the difficulty of reading mathematics will not be too surprised that these things happen.
Mathematician Kevin Buzzard worked until 2017 in algebraic geometry. Cases like the above of Zhang’s proofs lead him to try to find a remedy to this situation. In fact, checking a proof, verifying it, is a mechanical task for which algorithms exist, while none are known for the creation of proofs.
Buzzard found that programs already existed to verify the implementation of algorithms on computers (when we fly in an aeroplane we are trusting our physical integrity to programs that must be reliable). These programs are also used to check mathematical proofs. Buzzard chose one of these existing programs: Lean.
In order for a computer to verify a proof, it is necessary to teach the computer the mathematics used in the proof. That is, the computer must know the definitions above and the main theorems. For this reason, the first task is to “teach” undergraduate mathematics to the computer. In this task, it confirms that the proofs of all these theorems are correct. This is the aim of the Xena project led by Buzzard.
The challenge: Liquid Tensor Experiment
Few in the general public will have heard of Peter Scholze.
At the age of 16 he learned of Wiles’ proof of Fermat’s last theorem and set out to understand it. This motivated him to follow a special path to study what he needed for that purpose. Today, at the age of 33, he is a star among mathematicians. One of his first successes (at the age of 22) was to simplify a proof that took up a 288-page book written by Michael Harris and Richard Taylor, reducing it to a 37-page paper. Today, he is a Fields Medal winner for his creation of the perfectoid spaces, which are a tool that has already borne much fruit in algebraic geometry.
On 5 December 2020, he published a challenge on the website of the Xena project promoted by Buzzard to teach mathematics to Lean:
Prove the following theorem:
Theorem. (Clausen, Scholze) Let \(0<p'<p\le 1\) two real numbers and \(S\) a profinite set and let \(V\) be a \(p\)-Banach space. Let \(\mathcal M_{p’}(S)\) be the space of the \(p’\)-measures over \(S\). Then $$\text{Ext}^i_{\text{Cond}(\text{Ab})}(\mathcal M_{p’}(S), V)=0$$ for all \(i\ge 1\).
Scholze explains in his post on Buzzard’s blog the importance of the theorem in his attempt to turn classical functional analysis into a branch of algebra. Also that the proof of this theorem is extraordinarily complicated, so that he still has some doubts. More precisely, Scholze is “99.9% sure” that his proof is correct. But the result is basic for further work; it will be used in the future as a black box. Those who use it will have no real motivation to check it. And this is why it is especially important to be completely sure of its validity.
The answer to the challenge
Scholze’s challenge was taken up by a group of mathematicians led by Johan Commelin, who in record time have managed to formalize a large part of the proof.
A few days ago, on 5 June, Scholze posted again on Buzzard:
While this challenge has not been completed yet, I am excited to announce that the Experiment has verified the entire part of the argument that I was unsure about. I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research.
Scholze goes on to explain the process in more detail. In order to verify the proof, it has to be broken down into small steps. This leads to a greater degree of understanding. Scholze explains: When I was trying to demonstrate the result, part of the difficulty is that I was unable to retain all the details in my RAM. He means having all the details present simultaneously. The experiment made the proof considerably more explicit and more elementary.
Leibniz’s dream come true
Leibniz was a master of notation. To him we owe the notation $$\int f(x)\,dx$$ to represent the area defined by a function (what, by adding the limits of integration, today we call Riemann integral). But Leibniz dreamed of a symbolic language like mathematics, so that, expressed in that language, any controversy would be reduced to a mere calculation as in mathematics. Later, logicians have shown that the verification of a formal proof is indeed a mere calculation, for which an algorithm can be devised. We can say that the Scholze-Buzzard experiment is the first example in which a controversy is decided by a calculation. The proof has been verified mechanically. The experiment is the achievement of Leibniz’s dream. Only Leibniz already took it for granted that in mathematics there was no controversy, and he was thinking of any subject in life, politics or morals.
But we have already seen that there is controversy in mathematics. Mathematicians do not write formal proofs. We don’t need to make many steps explicit. That is necessary, otherwise the proofs would have many steps that are somewhat irrelevant and that would make the proof impossible and tedious for a (human) person.
One thinks of the possibility that in a few years the refereeing process will be automated. That an article will not be accepted until its proofs are verified by Lean or any other proof checker deemed convenient. I don’t think that’s far off. We practically have the means.
Now we will enter a much more speculative terrain, but one that I can’t help thinking about.
Feynman and artificial intelligence
Feynman (1918-1988) was a Nobel laureate in physics and a really interesting personality. (Anyone who doesn’t know him should read a chapter of his physics course, you’ll probably want to read some more, and you can also check out the book Surely you’re joking, Mr. Feynman!) In 1985, in a lecture, Feynman answers an audience member’s question: Do you think there will ever be a machine more intelligent than a person? In his answer, Feynman gives the example of interpreting images. Things that a person does instantaneously are very difficult. He does not claim that they will never come, but that we do not know how to make a machine recognise patterns, shapes or configurations. A few years have passed since then. Feynman would be surprised today to see that computers already replace humans in driving cars; will they ever replace humans in mathematical creation? And in artistic creation? These are disturbing questions. But no more than 30 or 40 years have passed between the digitalisation of the first image and the ability to interpret them in real time to leave the driving of a vehicle in their hands.
The Scholze-Buzzard experiment is like the beginning of the digitisation of proofs. We do not know whether once the Lean programme learns all the mathematics that a doctoral student studies, it will not be possible for a different process to start.
Mathematical creation
We have seen that the verification of a demonstration is a mechanical task, but not its creation. Lean needs the proof to verify it. But, for example Scholze, how does he prove the theorem? Here we have an example of the problem \(P\ne NP\). Given a mathematical statement \(T\), we ask is \(T\) a theorem, is there a proof of \(T\) of length \(<C\)? If we are given the proof, a mechanical program will give us the answer to this question (verifying the proof), in a time proportional to \(C\).
But if we are given only the statement \(T\), the only algorithm we know to obtain the proof is to write down all possible combinations of symbols of length \(<C\) and check whether or not each of those combinations is a proof. Such an algorithm would take too long.
We say that \(P= NP\) if whenever we have an algorithm to validate the solution to our problem in reasonable time, we can also generate the solution in reasonable time. In our case that would be saying that we can generate the proof in reasonable time. Everybody thinks that this is not the case, that \(P\ne NP\). That to generate the proof you need a genius, like Scholze.
The algorithm nobody wants to see
Mathematical practice tells us that problems can be solved, that it is not so difficult. Questions that at the time seemed impossible, such as squaring the circle, Fermat’s last theorem, the continuum hypothesis, Poincaré’s conjecture and a long etcetera, have been solved, either with a solution or having demonstrated its impossibility with the current axioms. The proof has taken a long time to obtain, but we cannot say that this solution has taken very long in relation to the length of the proof, which is the important thing here.
And, above all, we have an algorithm, an algorithm that nobody seems to see. First of all, we have the brain. How does a creative mathematician act? He studies the related concepts, the proofs of the fundamental properties of these concepts. This gives life in his brain to images that boil inside his mind, collide and intertwine. This boiling state is often generated by the desire to solve a concrete problem, the images become clearer and clearer. They come to life, they are born, grow and die. There are many descriptions of this situation, and the experience of each mathematician is not always the same. We can highlight Poincaré’s in his book Science and Method in the chapter devoted to mathematical creation. Wiles has also given us a description:
Perhaps I can best describe my experience of doing mathematics in terms of a journey through a dark unexplored mansion. You enter the first room of the mansion and it’s completely dark. You stumble around bumping into the furniture, but gradually you learn where each piece of furniture is. Finally, after six months or so, you find the light switch, you turn it on, and suddenly it’s all illuminated. You can see exactly where you were. Then you move into the next room and spend another six months in the dark. So each of these breakthroughs, while sometimes they’re momentary, sometimes over a period of a day or two, they are the culmination of—and couldn’t exist without—the many months of stumbling around in the dark that proceed them.
The algorithm for solving the mathematical problems and finding the proofs of the conjectured theorems is as follows: take young people who are motivated by mathematics, show them the conjectures, propose related problems that are within their reach. Suggest that they study the related works and related tools. Let them dream and in a few years they will have found the proofs or built buildings and tools with which the next generation will be better equipped.
The method is completely reliable.
This problem of building demonstrations is NP-complete. This means that, if this algorithm exists, it must be able to solve any problem in the \(NP\)-class. If this algorithm is correct, then \(P=NP\).
Artistic creation
Someone will think that I am talking only about mathematical creation. But it is essentially the same situation. Let’s think of Mozart as a child, his father, a musician by profession, gave music lessons to his older sister, Mozart being still a baby listened to his father, and watched his sister, playing melodies and scales on the piano… It is not surprising that these melodies entered his head, and found the completely plastic mind of a child. Another might have abhorred music, but he was not forced in the least and his mind was shaped for music. It is the same process I indicated before, one begins by reading mathematics and appreciating the beauty of the proofs, at a given moment the mathematical ideas and proofs begin to boil, to seethe, forming new combinations. The main difference is that of what a mathematical proof is we have a precise definition, of what a melody is, our idea is not so well formed. But, if you think about it, even musical styles are like differences in the definition of what a perfect melody would be.
I think anyone can do mathematics, or make music, or write. The problem is that the first thing you need is motivation. A motivation that has to be deep. Most people simply have other motivations. Mozart’s case is special, as any other case would be.
The process that is happening now with the Lean programme is similar to what is happening in the mind of a mathematician in training. In 10 or 20 years we will know whether the process remains at that point or whether computers will be able to create mathematics. Kevin Buzzard is sceptical, but Christian Szegedy, who is prominent in the area of Artificial Intelligence, thinks that in 10 years computers will beat mathematicians in proving theorems.
Learn more
Scholze’s two posts on Xena project: Liquid tensor experiment; Half a year of the Liquid Tensor Experiment: Amazing developments.
Information about Lean can be found in: Kevin Buzzard’s lecture on Lean. (At minute 35 onwards he talks about the possibility of computers finding mathematical proofs).
If you want to learn Lean, to be able to use it, maybe you can begin with Starting with Lean.
Kevin Buzzard also explains the \(P=NP\) problem in connection with these ideas: Kevin Buzzard’s lecture presenting \(P\ne NP\).
Feynman’s lecture, Richard Feynman, can machines think? or The whole lecture. Feynman shares my idea that there is not such thing as geniuses.
We can find on the web several exposés about the Scholze-Buzzard experiment: Article in Nature about the Scholze-Buzzard experiment, or also on Quanta magazine.
The featured image is taken from Scholze’s entry, perhaps representing the monster of his demonstration.
Leave a Reply