mlsanityData to 7 Oct 2026

Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization

arXiv 2609.39228 ↗First posted 30 Sep 2026cs.AIcited by 0

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 36 of its 48 references that are in the map. First posted on arXiv 30 Sep 2026.

Builds on

36 of 48 references.

References · 36

  1. 2023G-Eval: NLG Evaluation using GPT-4 with Better Human Alignmentcited by 2,205
  2. 2024SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineeringcited by 1,628
  3. 2024OpenHands: An Open Platform for AI Software Developers as Generalist Agentscited by 956
  4. 2023Prometheus: Inducing Fine-grained Evaluation Capability in Language Modelscited by 558
  5. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  6. 2025Rubrics as Rewards: Reinforcement Learning Beyond Verifiable Domainscited by 328
  7. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  8. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  9. 2022Autoformalization with Large Language Modelscited by 252
  10. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  11. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  12. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
24 more
  1. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  2. 2025Checklists Are Better Than Reward Models For Aligning Language Modelscited by 115
  3. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  4. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  5. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  6. 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematicscited by 43
  7. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  8. 2025APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoningcited by 34
  9. 2024A Semantic Search Engine for Mathlib4cited by 30
  10. 2026Automated Conjecture Resolution with Formal Verificationcited by 21
  11. 2024FormalAlign: Automated Alignment Evaluation for Autoformalizationcited by 19
  12. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 18
  13. 2026M2F: Automated Formalization of Mathematical Literature at Scalecited by 12
  14. 2026LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalizationcited by 11
  15. 2025Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalizationcited by 9
  16. 2026QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problemscited by 9
  17. 2025ASSESS: A Semantic and Structural Evaluation Framework for Statement Similaritycited by 8
  18. 2025The Equational Theories Project: Advancing Collaborative Mathematical Research at Scalecited by 8
  19. 2026Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Provingcited by 7
  20. 2026Automatic Textbook Formalizationcited by 5
  21. 2026Formalizing Mathematics at Scalecited by 5
  22. 2026Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalizationcited by 4
  23. 2026FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Modelscited by 2
  24. 2026SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalizationcited by 2

Built on by

Not cited yet.