This is an opinion piece based on my research and ideas. I recently read the paper by Alex Kontorovich, The Shape of Math To Come, which inspired me to contemplate the future of mathematics and mathematicians. However, I will not go into as much detail, but rather state a high-level overview of ideas.
Autoproving vs Autotranslation
Before we start, we need to differentiate between autoproving, giving a formalized proof to a formalized statement, and autotranslation, the act of taking an informal statement (such as the definition of a Vector Space or a Conjecture) and transferring it into a formalized language like Lean.
A notable observation is that, autotranslation lacks inherent verification and cannot be fully automated. While AI can translate natural language into formalized language (such as Lean), no formal proof exists to confirm that the formalized statement matches the informal intent. A human must still manually verify that the resulting symbols correctly represent the original mathematical idea.
Autoproving, on the other hand, can be completely automated; given a formalized statement, we can trust the formalized proof to be correct. This is, of course, assuming that the environment in which the verification happens is immune to reward hacking or adversarial attacks on the verification. Making verification robust is a problem which the Lean FRO is well aware of, with the latest addition being the Comparator Verifier.
There is also autoformalization, which can be seen as autotranslation followed by autoproving.
Math Singularity
I want to introduce a thought experiment involving an autoproving system capable of proving anything that humanity has ever formalized, and enabling the proof of any new formalized statement in a matter of minutes or hours. Such a system, which I will just dub "Math Singularity", would be the extreme end along a spectrum of autoproving abilities.
What would doing mathematics look like with such a system at our disposal? Would it mean that we are only formalizing statements, building and exploring theories, and rapidly answering any question we formalize? Developing a big program or theory such as the Langlands Program would probably much more resemble the workflow or contributions of human mathematicians.
One can, of course, also argue that a system capable of proving everything known to humanity could also be engineered and utilized to create entirely new theories and complete new fields of mathematics, but that would be of no use to humans. We need humans to interpret it to advance the knowledge corpus of humanity—unless we simply decide to hand off the interpretation and utilization of these scientific advancements in math completely to AI, at which point we would have to raise entirely different questions.
How might this transition look like?
We can roughly sketch the spectrum of autoproving capabilities as follows:
I define MST (Mathematical Superintelligence) as a system vastly more intelligent than the most intelligent human mathematicians, while still being unable to prove extremely hard problems such as the Millenium Problems or the Landau Problems.
We are currently at a point where small theorems can be independently proven, such as a recent Erdős problem as documented by Terence Tao's Mastodon Post. The further we proceed along the spectrum of autoproving, the less proofs become the bottleneck, enabling humanity to explore the mathematical landscape more throughly.
Currently, informal (natural language) math is advancing faster than formalized math. If autoproving systems become better, it will be of benefit for frontier mathematicians to formalize their current area of research to leverage these systems' capabilities. Consequently, more projects and workshops will likely emerge to formalize frontier research fields within Lean. In this vein, Lean serves as the interface for autoproving systems, while also providing the benefit of formalized correctness into frontier research.
How might human collaboration and papers develop?
Mathematicians write papers to introduce new knowledge, an important ingredient being a correct proof, ensuring the newly introduced theorems and knowledge are consistent with the existing knowledge corpus. Moving along the autoproving spectrum will lead to higher abstraction, where proofs of smaller lemmas fall into the background by being a Lean reference, and results provable by autoproving systems are not worthy of their own paper anymore.
There will most likely still be hybrid proofs for statements outside of the current reach of autoproving systems, where humans supplement by providing structure or insight to the proof to various extents.
Integrating vast databases of formalized proofs into existing academic frameworks presents another significant hurdle. While Mathlib is an easy example, its current architecture may face scalability issues when attempting to encompass all of humanity's mathematical knowledge. We may see a evolving field of different institutional databases, or a unified repository similar to arXiv for preprints might eventually crystallize. These are all problems which can be solved, but must be tackled to enable more proper utilization of autoproving systems.
Current Advancements
Lean is currently the most used programming language in the realm of formalization of math and will likely stay the most relevant language for the foreseeable future, serving as the foundational layer for these advancements.
Regarding the development of AI systems for autoproving, DeepMind and Harmonic AI are currently the biggest labs in the field, with Alphaproof and Aristotle respectively. However, there are many teams at various labs and smaller companies working on autoproving systems, such as ByteDance with Seedprover or Alephprover from Logical Intelligence.
Summary
Math as we know it is about to change, and I think many are feeling that.
The synergy between Math and Lean represents a unique opportunity for unbound continual learning, as its formal environment allows for continuous improvement independent of real-world constraints.
If we can overcome these remaining challenges of scaling formalization, we may soon witness a golden age of results in mathematics.
Edit 1: I have switched the naming of Autoformalization for Autotranslation following a comment made by Alex Kontorovich.