Fyan: A Human–AI Harness with Semantic Auditing for Document-Level Formalization
Wei Zhao, Yangshuo Zou, Chengxiang Ding, Yifan Wu, Xuchuan Wang, Zimu Mao, Lei Zhang, Tao Luo
cs.AI
Sep 30, 2026 · v1
TL;DR
Builds an LLM agent harness that formalizes whole mathematical documents into dependency-linked Lean 4/Mathlib projects, evaluated with strict Lean checking.
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.
Problem
Scaling autoformalization from isolated theorems to whole documents requires managing dependencies and reusing results. Semantic mismatches between formal and informal statements can also propagate through downstream proofs even when everything compiles.
Approach
Fyan coordinates Specifier, Reasoner, Planner, Formalizer, Curator, and Auditor components over a document-level dependency DAG, producing a Lean project with provenance and review records. Its semantic audit has an LLM build structured evidence about correspondences, omissions, scope, and logical relations, which a deterministic validator then grades. Any accepted substantive deviation must come with a Lean-checked proof-transfer obligation linking it back to the source. All stages use the same model, DeepSeek-V4.1-Flash, with Lean 4.32.2 and Mathlib.
Results
Using the same model as the baseline, Fyan proves 86/143 FormalTCS theorems under strict Lean checking versus 69 for a general agent harness, and raises the natural-language proof score from 0.501 to 0.851. On ConsistencyCheck its audit reaches recall of 0.777 versus 0.636 for a direct LLM judge on verified labels. It also built ODENumLib, a 9,355-line Lean library on numerical analysis of ODEs.
| Task | Metric | Control | Fyan | Difference |
|---|
| FT2FP | strict Lean pass | 69/143 (48.3%) | 86/143 (60.1%) | +17 |
| T2NP | rubric mean | 0.501 | 0.851 | +0.350 |
| NT2FT | BEq+ equivalent | 5/143 (3.5%) | 8/143 (5.6%) | +3 |
FormalTCS stage-wise results (same model)
