AI for Mathematics

Tools to inspect, audit and steer AI-assisted formalization and proof writing

Large language models can now draft, formalize and revise mathematics, but a result that compiles or reads well is not the same as a result that is correct, faithful and understood. This project develops human-centered tools to inspect, audit and steer AI-assisted mathematics. Lea is an agent backbone that lets mathematicians keep control while an agent formalizes research-level mathematics in Lean, with LeaChat and LeaOverleaf as front ends. LeanTrail audits what has actually been formalized by aligning the items of a paper with Lean declarations and checking proof completeness deterministically. ProofDiff compares informal, AI-generated proofs by building source-grounded argument maps and proposing correspondences between them for human review. Together, these systems combine language models with visualization and deterministic checks so that people can see what an AI system proved, how it argued, and where it departed from the source.