Preprint Open access
FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification
Coding agents increasingly automate Lean proof development, but successful compilation alone does not establish that a candidate proves the intended statement under acceptable assumptions. We present FORALL-LEAN-AGENT, a frontend-agnostic framework for auditable reasoning in formal mathematics and software verification …