New system tackles mathematical formalization bottleneck, achieving 68% accuracy on theorem translation

Researchers have introduced Aria, an automated system designed to address a critical challenge in computational mathematics: reliably translating informal mathematical statements into formal code that machines can verify. The work tackles a persistent limitation of large language models—their tendency to hallucinate details, mismatch semantic meaning, and struggle to define novel concepts when formalizing theorems.

How Aria works#

The system operates through a two-phase reasoning process modeled on how expert mathematicians approach formalization. Rather than attempting direct translation, Aria recursively decomposes mathematical statements into a dependency graph—breaking down complex conjectures into their constituent parts and dependencies. It then reconstructs formal statements in the Lean proof assistant starting from grounded, verified concepts.

To ensure accuracy, the team developed AriaScorer, a verification layer that retrieves authoritative definitions from Mathlib (a repository of formalized mathematics). This grounding mechanism checks term-level correctness and guards against semantic drift.

Benchmark performance#

Testing across multiple datasets reveals significant improvements:

• ProofNet: 91.6% compilation success and 68.5% final accuracy, outperforming prior approaches
• FATE-X (algebra problems from research literature): 44.0% accuracy versus 24.0% for the best existing baseline
• Homological conjectures dataset: 42.9% accuracy while competing methods scored zero

The strong results on specialized algebraic problems and homological conjectures suggest Aria handles niche mathematical domains more effectively than general-purpose baselines.