2 papers
cs.AI2026
ProofDiff: Auditable Argument-Level Comparison of AI-Generated Mathematical Proofs
Matan Tsafrir, Esdras Medeiros, Jorge Poco +3
Mathematical understanding depends on the route from hypotheses to conclusion: how the parts of a proof function and which dependencies carry the argument forward. This structure c…
cs.HC2026
Lea: An Agent Backbone for Mathematician-Controlled Formalization in Lean
Shaswat Patel, Daniel Aarao Reis Arturi, Kevin Gomez +6
Agentic systems now formalize research-level mathematics in Lean, but they are built for autonomy: the mathematician states a target and inspects a result. The alternative, a gener…