Beyond the Library
An Agentic Framework for Autoformalizing Research Mathematics
Arshia Soltani Moakhar · Iman Gholami · Max Springer · Mahdi JafariRaviz · MohammadTaghi Hajiaghayi
University of Maryland · Princeton University
👤
🤖
→
Theorem. ∀ n ≥ 2 ...
Proof. ... ∎
A mathematician, or an AI, writes a proof of a hard theorem.
Verifying that a proof is correct is hard and slow.
theorem main : P → Q :=
by intro h; exact ...
✓ no goals
Lean can verify a proof mechanically, in seconds.
So we need to translate the mathematics into Lean.
Theorem. For every … there exists c > 0 such that …
needs
concept 1
concept 2
concept 3
A research theorem rests on concepts Lean doesn't have, so we pin down each one.
concept 1 · v1
✓✓✓
chosen ✓
concept 1 · v2
✓✓✗
a lemma can't be proved
We formalize each concept, keeping the version whose auxiliary lemmas can all be proved.
✓ concept 1
✓ concept 2
✓ concept 3
→
theorem main_theorem :
∃ c, 0 < c ∧ …
:= by ...
With the concepts in place, we assemble the main theorem.
A prover drafts a proof; a critic attacks it until it holds.
🌳 main theorem
lemma A
lemma B
📚 prior work
We break the proof into named lemmas (prior work is cited, not reproved).
intro h
have h₁ := lemma A
have h₂ := lemma B
✓ proved
Lean ✓ compiles
🔁 then recurse on lemma A & B
The agent proves each node from its sub-lemmas, then recurses on those lemmas, all checked by Lean.
A sharp version of Talagrand's selector process conjecture and an application to rounding fractional covers
STOC 2025
formalized🐛 gap found
Refuting the Direct Sum Conjecture for Total Functions in Deterministic Communication Complexity
STOC 2025
formalized
Approximation Guarantees of Median Mechanism in ℝᵈ
STOC 2025
formalized
A generalized trace reconstruction problem: Recovering a string of probabilities
STOC 2025
formalized
Efficiently learning mixtures of two Gaussians
STOC 2010
formalized
Beyond the Library
An Agentic Framework for Autoformalizing Research Mathematics
Arshia Soltani Moakhar · Iman Gholami · Max Springer · Mahdi JafariRaviz · MohammadTaghi Hajiaghayi
University of Maryland · Princeton University