AxiomProver: When Mathematical Intuition Meets the Formalization Wave

Forum topic · ✨步子哥 · 2026-01-10

Summary

AxiomProver, an AI system developed by a team led by 24-year-old Carina Hong, achieved a perfect 120/120 score on the 2025 Putnam Competition by producing complete, machine-verifiable proofs in the Lean theorem prover. This analysis explores how the system translates human mathematical intuition into formal Lean code, with detailed case studies: a 2,054-line induction proof (518 minutes) for problem A5, a 5-hour brute-force attack on p-adic numbers in A6, and a 400-line geometry proof without diagrams for B1. The post contrasts two cognitive styles — human top-down abstraction, likened to Grothendieck's 'rising sea,' versus AI bottom-up enumeration in the Turing tradition — arguing the two are complementary rather than competitive. It also covers reactions from Terence Tao, who called AI's resolution of an Erdős problem a milestone, and mathematician Bartosz Naskręcki's amazement at GPT-5.2 Pro. All proofs are publicly available on GitHub for community audit, positioning AxiomProver as a human-AI collaboration tool rather than a replacement for mathematicians.

Introduction: An 'Impossible' Declaration

In June 2025, Carina Hong and her team spent three months trying to get AI to *understand* why the angles of a triangle sum to 180 degrees — not compute it, not memorize it, but understand it. Frustrated that a truth humans explain with a single diagram required 200 lines of machine code, they pressed on. Six months later, AxiomProver scored 120/120 on the 2025 Putnam Competition.

> AxiomProver = Axiom + Prover + X — an "AI mathematician" that writes Lean proofs. In plain terms: an agent that can "see" mathematical structure and translate it into machine-verifiable code.

Architecture

The pipeline: Human intuition → AI translation → Lean verification → public GitHub audit.

Input: competition problems (Putnam 2025, 12 problems, 6 hours)
Processing: symbolic reasoning and formalization by AxiomProver
Output: complete proofs verifiable in Lean
Storage: all proofs published on GitHub for community review

The Data: A Quantitative Archaeology of Proofs

| Problem | Human perception | AI perception | Lean LOC | Time | Deciding factor | |---------|------------------|---------------|----------|------|-----------------| | A2 | Easy (see the figure) | Tedious (definitions) | ~200 | - | Humans win on intuition | | B2 | Easy (lemma) | Tedious (60+ line proof) | ~150 | - | Humans win on concision | | A5 | Medium (induction) | Extremely tedious (bookkeeping) | 2054 | 518 min | AI wins on patience | | A3 | Hard (combinatorics) | Easy (no branching) | ~300 | - | AI wins on logic | | B1 | Hard (geometry) | Medium (symbols) | ~400 | - | AI wins on algebra | | A6 | Very hard (p-adics) | Hard (brute force) | High token | 5 hours | AI wins on persistence | | A4 | Medium (algebra) | Medium (geometry) | ~500 | - | Different approaches | | B4 | Medium (diagram) | Tedious (enumeration) | 1061 | - | Different approaches |

Cognitive Topology: Two Geometries of Thought

Human mathematics follows Grothendieck's "rising sea": discover patterns, abstract them into definitions, build theories, then solve specifics — top-down, from general to particular.

AI mathematics follows Turing's brute-force tradition: enumerate the search space, verify each candidate in Lean, find a path through combinatorial explosion — bottom-up, from particular to general.

These modes are not comparable but complementary. Hong's vision: humans supply inspiration, machines supply verification, and the two spiral upward together.

Three Approaches to the Singularity

1. GPT-5.2 Pro's absurdity — Polish mathematician Bartosz Naskręcki observed that it's hard to find a genuinely non-trivial problem where the model gets stuck, joking: "Either OpenAI has a team of around-the-clock elves and top mathematicians doing live ghost-solving, or the model has genuinely solid capability." A reverse Turing test: humans suspect there are humans behind the machine. 2. AxiomProver's brute-force elegance — The A6 victory took 5 hours and near-record token usage, using "a particularly clumsy but genuinely effective method" for p-adic expansion. When inspiration runs dry, endurance becomes creativity. 3. Terence Tao's milestone — Tao called AI's resolution of an Erdős problem a milestone. If AI can autonomously solve Erdős problems, Millennium Problems (P vs NP, Riemann Hypothesis) may not be out of reach. But Tao remains cautious: a milestone ≠ singularity. The singularity requires a self-improving loop — today's AI is a tool, not an agent.

Controversies

Is this "real understanding"? Critics say it's pattern matching; supporters reply that human mathematicians do pattern matching too — we call it intuition. AI's understanding is syntactic, human understanding semantic, yet at sufficient complexity they become behaviorally indistinguishable.
Is Lean "math enough"? Formalization exacts a tax: 60 lines to prove a positivity lemma, 2,054 lines and 518 minutes for one induction. But that's Lean's value — it forces you to check every "obvious."
Will AI replace mathematicians? Hong's answer: "We don't need to storm every problem head-on. Human intuition + machine verification = a rising sea." Not replacement — division of labor.

Conclusion

For centuries mathematics was "humans speak, humans listen." Now a third voice exists — machine proposes, human verifies, machine iterates. AxiomProver turns mathematics from a monologue into a dialogue: a bridge between formality and intuition.

Quick Reference

| Concept | Human way | AI way | Metaphor | |---------|-----------|--------|----------| | Proof | Inspiration → construction | Enumeration → verification | Architect vs construction crew | | Difficulty | No inspiration = no solution | High tokens = hard problem | Poet's bottleneck vs compute bottleneck | | Geometry | Visual intuition | Symbolic algebra | Painter vs algebraist | | Combinatorics | Clever construction | Branch-free search | Magician vs exhaustive searcher |

Project: https://axiommath.ai Proofs: https://github.com/axiommath/proofs Founder: Carina Hong License: AI + Human Collaboration

> *"Mathematics is not a clever game of symbols, but the patient excavation of truth."* — From Hilbert to Lean to AxiomProver.