AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness

Excerpt

arXiv:2610.05367v1 Announce Type: cross Abstract: Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Despite rapid progress, research-level proofs often depend on concepts missing from leading proof assistant libraries (e.g., Lean's Mathlib), and successful compilation does not guarantee that a translation preserves the theorem's meaning or the proof's reasoning. Furthermore, aligned NL-FL trai