Fyan system improves accuracy and oversight in formal math proofs
Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization
Artificial Intelligence
Summary
Mathematical proofs written by computers often miss details or don't fully match the original ideas. The authors present FYAN, a system that helps humans and AI work together to formalize math proofs more accurately, checking entire documents rather than single theorems one by one. FYAN uses a language model to find and explain differences between informal statements and their formal versions, and a validator to confirm these checks, helping spot errors and better align the formal proofs with original intentions. This approach improved proof success rates and consistency checks compared to other automated methods.
What this means in practice
- •For software verification engineers: Assist software engineers in creating and auditing formal proofs for software correctness by coordinating AI and human inputs with semantic error detection.
- •For automated theorem proving teams: Provide tooling that improves theorem proving workflows and error-checking for document-level mathematical formalizations using consistent AI-driven semantic audits.
Authors
Wei Zhao, Yangshuo Zou, Chengxiang Ding, Yifan Wu, Xuchuan Wang, Zimu Mao, Lei Zhang, Tao Luo
Abstract
We present FYAN, a human--AI harness for document-level mathematical formalization. Rather than treating theorems in isolation, FYAN coordinates an end-to-end workflow spanning specification, proof planning, logical review, Lean proof construction, knowledge curation, and validation, with support for independent supervision and human guidance. A central component is evidence-grounded semantic auditing, which assesses whether formal statements faithfully preserve their informal specifications. A language model constructs structured evidence over local correspondences, omissions, scope, and logical relations, while a deterministic validator checks this evidence and produces reproducible judgments. When a substantive but admissible deviation is accepted, FYAN requires an explicit proof-transfer obligation connecting the formal statement back to a source-facing interpretation. With the same model (DeepSeek-V4.1-Flash) in every stage, FYAN proves 86 of 143 FormalTCS theorems under a strict Lean check, against 69 for a general agent harness, and raises the natural-language proof score from 0.501 to 0.851. On ConsistencyCheck, its semantic audit catches more inconsistent statements than a direct LLM judge, both on labels verified against the source (recall 0.777 vs. 0.636) and on the original labels (0.873 vs. 0.820), and localizes each mismatch it reports to a specific hypothesis, conclusion, or scope. FYAN also built ODENumLib, a 9,355-line Lean library for the numerical analysis of ordinary differential equation.