Remind Me: What’s the Enormous Theorem?
Benjamin Skuse
Efim Zelmanov (1994 Fields Medal) is an excellent orator, capable of elucidating any mathematical topic with such knowledge and enthusiasm as to make it feel like the most important and consequential subject you have ever been exposed to.
The first time I heard him speak was at the 2024 Lindau Nobel Laureate Meeting, where his Heidelberg Lecture ‘What Do Mathematicians Think About?’ highlighted his admiration for early 19th Century French mathematician Évariste Galois, as well as his deep appreciation of beauty in mathematics.
Group Theory 101
‘Algebra: Basic Constructions’ – the title for his Laureate Lecture at the 13th Heidelberg Laureate Forum – suggested a talk with less general appeal, likely a technical deep dive into abstract algebra and, most likely, group theory; a topic that I confess to have always regarded as impenetrable and dry.
But I should not have worried. Though my predictions were correct, starting from very basic principles, Zelmanov immediately elucidated the motivation for the creation of groups and group theory in an accessible way. In the 19th Century, polynomial equations of degree 2 (quadratic equations), 3, and 4 were already known to be generally solvable, but no equivalent algebraic general formula had been found for any higher-degree equations.
It was Galois who broke this impasse, through the idea of the group; a set of elements combined with an operation (like addition or multiplication) that follows specific rules. “A group is one of the most fundamental concepts in mathematics – if you are going to a desert island and you can only take three mathematical concepts with you, think about taking a group,” joked Zelmanov. “[But] at that time, there was no general concept of a group.”
Galois changed this by introducing new mathematics to allow the study of groups of symmetries of polynomial equations. With these tools, he managed to explain why it is possible to solve some equations, including all those of degree four or lower, and why it is not possible for most equations of degree five or higher.
From these foundations, group theory and its main building block – finite simple groups – were born. Finite simple groups are, as the name suggests, finite, and cannot be reduced or simplified further. They are analogous to prime numbers being the building blocks of integers. “[This] started the biggest programme in algebra, maybe the biggest programme in mathematics ever: find all finite simple groups,” exclaimed Zelmanov.
Finding All Finite Simple Groups
After Galois discovered the first finite simple groups, Zelmanov explained that a whole alphabet of groups were slowly found over the course of more than a century, many with order as large as desired (though not infinite – they just have no upper bound on size and are hence often labelled infinite families). This effort resulted in infinitely many simple finite groups that can be divided into four categories: cyclic groups of prime order; alternating groups; groups of Lie type; and sporadic groups (exceptional groups that do not fit into infinite families).
Of the latter, Zelmanov made special mention of the Monster group, the largest of the sporadic groups, which was discovered in 1973 and stands at an approximate size of \(8.08 \times 10^{53}\) elements. This group is of interest not just for its size but also for its surprising connection with modular functions from number theory.
More specifically, the Monster group can be represented by matrices of size \(196,883\) and no less, and the first few coefficients of the \(j\)-invariant modular function are \(196,884\): precisely equal to \(196,883 + 1\). When told about this link, English mathematician John Conway reportedly replied that it was ‘moonshine’ and the term stuck. Today, it is referred to as ‘monstrous moonshine’.
Soon after the discovery of the Monster group, work began on proving that all simple finite groups belong to the four categories mentioned earlier. “In 1982, the classification of finite simple groups had been announced, but actually the final publication appeared in 2011,” said Zelmanov. “Now it is all published – more than 10,000 pages.”
The Classification of Finite Simple Groups, or the ‘enormous theorem’ as it is colloquially known, proves and documents a definitive, complete list of all the finite simple groups. It is a proof like no other. It is not just a simple geometric construction, symbolic calculation, numerical algorithm, or any other recognisable proof. Instead, it brings together results and arguments from several hundred journal articles written by around 100 authors over a half-century period that far exceeds what any individual mathematician can fully absorb.
But its size and completeness are also a pointed problem. As it is considered ‘done’, young mathematicians don’t want to work on it, nor are they likely to be funded to work on it. At the same time, the authors of this pioneering work are starting to pass away, taking their specialist knowledge and expertise with them.
“Everybody will know that there is this great theorem … [but] when this generation goes, nobody will understand,” summarised Zelmanov. “It will be like Coca-Cola; we all drink it – nobody knows what it is made from.” Not only will this situation be sad for human understanding generally, but as the years go by, fewer and fewer people will be able to decipher and explain the proof’s deepest machinery, or fix errors or omissions if they come up.
Preserve and Protect
With these concerns front and centre, two paths are open to preserve the knowledge contained in the enormous theorem and simplify it so that it remains in the mathematical canon for generations to come.
The first of these is an extreme simplification exercise, commonly referred to ‘revisionism’. This started with the work of American mathematicians Daniel Gorenstein, Richard Lyons, and Ronald Solomon in the 1980s and continues to this day, with the latest 570-page volume published in 2023.
However, although considerably reduced in size compared to the first-generation proof, the most recent proof is already standing at over 5,000 pages in length. Learning and deeply understanding it therefore still represents a superhuman investment of time and effort.
This is why an alternative way of preserving the knowledge contained in the enormous theorem is appealing. Computer formalisation would involve translating the proof into a formal language like Lean. But this is no small feat.
In 2012, a Microsoft Research team fully formalised the Feit–Thompson theorem. This 255-page theorem is a key element of the enormous theorem and states that every finite group of odd order is solvable. Taking the team six years to complete, it represents the only part of the enormous theorem that has been fully formalised up to now. The full formalisation is expected to run to millions of lines of code.
Another problem with formalising the enormous theorem is that the revisionism project is not yet finished. Few would want to work on a formalisation project where the proof has not yet already been fully streamlined and made bug-free on paper.
All of this being said, only two more volumes need to be completed of the revisionism project. Moreover, formal libraries are growing by the day, and AI autoformalisation is an active area of investigation that has seen significant success in recent times, most notably in the formalisation of two proofs associated with 2022 Fields Medallists Maryna Viazovska and James Maynard. As a result, the idea of formalising the enormous proof sounds less fanciful than only a couple of years ago.
Though many are rightfully concerned with the march of AI into mathematical landscapes, this particular application could prove hugely beneficial. It would formally verify the enormous theorem or at least highlight where errors are so that they could be fixed. And when completed, it would preserve the work digitally in perpetuity, potentially making it available to AI which could help future generations in interpreting its contents. Perhaps after this last step, mathematicians will finally be able to say that the “Classification of Finite Simple Groups” is complete.
The post Remind Me: What’s the Enormous Theorem? originally appeared on the HLFF SciLogs blog.