An AI agent called Aria can now translate high-level mathematical conjectures into verified Lean code at accuracy rates that leave previous methods behind.
Aria works in two phases. First, it breaks a conjecture into a dependency graph — a recursive map of every concept the statement relies on. Then it builds the formal Lean code bottom-up from those grounded pieces. A companion module called AriaScorer checks each term against Mathlib, Lean's standard math library, to catch semantic mismatches before they propagate. On the ProofNet benchmark, Aria hit a 91.6% compilation success rate and 68.5% final accuracy. On FATE-X, a set of hard algebra problems drawn from research literature, it scored 44.0% versus 24.0% for the best prior baseline. On a dataset of homological conjectures, Aria reached 42.9% accuracy while every other tested model scored zero.
Auto-formalization matters because verified proofs are the gold standard for mathematical certainty — and writing Lean by hand is slow even for experts. If a system can reliably translate a conjecture stated in plain math into machine-checkable code, it shortens the path from "we think this is true" to "we can prove this is true." The homological conjecture result is the most striking: reaching nearly 43% on problems where rivals scored nothing suggests the dependency-graph approach handles structural complexity that flat LLM generation cannot.
The caveat worth noting: benchmark accuracy and real-world research utility are different things. A 68.5% final accuracy on ProofNet means roughly one in three attempts still fails, and research conjectures are often messier than curated benchmarks — so treat the numbers as a promising signal, not a finished tool.