Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Shape of Math To Come

Alex Kontorovich

TL;DR

The paper envisions an AI-assisted, formally verified future for mathematical practice in which quasi-autonomous multi-agent formalization accelerates library growth and enables working directly in formal systems. It analyzes the fundamental tension between rapid growth of natural-language mathematics and slower, effortful expansion of formal libraries, arguing that a combination of scalable AI tooling, comprehensiveness of Mathlib, and an optimized workflow is required for formal mathematics to become foundational. It discusses the practicalities and challenges of adopting formalization in research and teaching, including translation subtleties, verification guarantees, and new modes of mathematical communication, and it culminates in a cautiously optimistic projection of how a ‘proof-at-multiple-resolutions’ paradigm could transform collaboration and understanding. The work emphasizes that the ultimate value lies in AI augmenting mathematical intuition rather than replacing it, with progress measured by reductions in the formalization factor and by tangible improvements in the efficiency and reliability of mathematical practice.

Abstract

We present an overview of how certain computational tools currently interact with mathematical practice, and reflect on the implications for research mathematics in the short to medium term, as the field navigates the emerging age of AI and formal verification systems.

The Shape of Math To Come

TL;DR

The paper envisions an AI-assisted, formally verified future for mathematical practice in which quasi-autonomous multi-agent formalization accelerates library growth and enables working directly in formal systems. It analyzes the fundamental tension between rapid growth of natural-language mathematics and slower, effortful expansion of formal libraries, arguing that a combination of scalable AI tooling, comprehensiveness of Mathlib, and an optimized workflow is required for formal mathematics to become foundational. It discusses the practicalities and challenges of adopting formalization in research and teaching, including translation subtleties, verification guarantees, and new modes of mathematical communication, and it culminates in a cautiously optimistic projection of how a ‘proof-at-multiple-resolutions’ paradigm could transform collaboration and understanding. The work emphasizes that the ultimate value lies in AI augmenting mathematical intuition rather than replacing it, with progress measured by reductions in the formalization factor and by tangible improvements in the efficiency and reliability of mathematical practice.

Abstract

We present an overview of how certain computational tools currently interact with mathematical practice, and reflect on the implications for research mathematics in the short to medium term, as the field navigates the emerging age of AI and formal verification systems.
Paper Structure (28 sections, 3 equations, 16 figures)

This paper contains 28 sections, 3 equations, 16 figures.

Table of Contents

  1. Introduction.
  2. In the Year 2000...
  3. What is an LLM?
  4. Stochastic vs. Deterministic Problems.
  5. AI Capabilities Are Advancing Rapidly...
  6. ... But Even Perfect Scaling Is Insufficient.
  7. Formally Verified Mathematics.
  8. What is Lean?
  9. What is Mathlib?
  10. The Library Gap and AI Assistance.
  11. A Path Forward: Quasi-Autoformalization.
  12. The Architecture: Four Agents.
  13. The Decomposer: From Ideas to Scaffold.
  14. The Translator.
  15. The Solver: Closing Goals.
  16. ...and 13 more sections

Figures (16)

  • Figure 2.1: A snippet from Gowers2000
  • Figure 3.1: The bottom of a page from "Harry Potter and the Deathly Hallows" by J. K. Rowling
  • Figure 3.2: An LLM is a function from context (a sequence of tokens) to a likelihood distribution of potential next tokens
  • Figure 7.1: Different aspects of "Lean"
  • Figure 7.2: Proving a theorem in Lean.
  • ...and 11 more figures