Towards the Automatic Mathematician: The Past, The Present, and the Next Few Months Ahead (Yes, Really)Oberseminar Discrete Optimization
by
Arithmeum, Lennéstr., 2 - Gerhard Konow-Hörsaal
Arithmeum / Research Institute for Discrete Mathematics
Autoformalization, the automatic translation of informal mathematics into machine-verifiable formal statements and proofs, has been the unifying theme of my research since founding the N2Formal team in 2016 at Google ("into-formal" or "N²-formal," where N² nods to neural networks).
Our first major result, DeepMath, showed that deep sequence models could effectively guide premise selection in large formal libraries. This laid the foundation for co-training theorem proving and autoformalization. The vision continued through tactic prediction for higher-order logic, reasoning in latent space, and early LLM-based autoformalization. That work demonstrated that transformers could already translate non-trivial portions of competition-level mathematics into Isabelle/HOL.
Today, systems like the Gauss agent (Math, Inc.) are semi-autonomously formalizing advanced results, such as the strong version of the Prime Number Theorem in Lean. It generated tens of thousands of verified lines in roughly three weeks, work that would likely take a human team many months.
The progress is accelerating. In the next few months, the focus will shift from single-agent systems to multi-agent ecosystems where specialized AI agents collaborate, compete, and improve via carefully designed market mechanisms. Agents will trade conjectures, proofs, and predictions in a shared database, creating open-ended, incentive-aligned collective intelligence while building a vast repository of fully formalized and verified mathematics, and learning super-human reasoning skills along the way.
This Oberseminar takes place in the Gerhard-Konow-Hörsaal, Lennéstr. 2. Participants are invited to have coffee or tea in the lounge, 2nd floor, before.
S. Held, S. Hougardy, L. Végh, J. Vygen