FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification.

arXiv:2610.00885v1 Announce Type: cross Abstract: 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-LEA