Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization
Authors: Wei Zhao, Yangshuo Zou, Chengxiang Ding, Yifan Wu, Xuchuan Wang, Zimu Mao, Lei Zhang, Tao Luo
Organizations: School of Mathematical Sciences, Shanghai Jiao Tong University, Shanghai 200240, China · University of California, Berkeley, CA 94720, USA · Zhiyuan College, Shanghai Jiao Tong University, Shanghai 200240, China · School of Biomedical Engineering, Shanghai Jiao Tong University, Shanghai 200240, China · School of Materials Science and Engineering, Shanghai Jiao Tong University, Shanghai 200240, China · Institute of Natural Sciences, MOE-LSC, Shanghai Jiao Tong University, Shanghai 200240, China · CMA-Shanghai, Shanghai Jiao Tong University, Shanghai 200240, China
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.
Figures & tables
Figure 1: The Fyan workflow for document-level formalization. Specifier turns the source into theorem units and a document-level DAG; the Orchestrator schedules ready units based on theorem dependencies and regularly checks ongoing proofs. Within each unit, models propose and deterministic gates decide: the semantic audit (Figure 2 ) freezes the statement produced by Formalizer or returns it for repair, and the completion gate accepts the proof, whose module is then reused downstream. Human guidance and Curator skills are advice only; Auditor writes a report for human inspection.
Figure 2: The Fyan semantic audit. The Fyan Judge, an LLM, first extracts a quoted, independently reviewed formula tree of N , then pairs the slots (objects, hypotheses, claims) that code cuts from it and from S1 , with a grade si per paired group. Code derives polarity, checks the record, and routes S1 by the statement grade minisi : at or above the threshold (default 2) it is frozen for the document-level project, else repaired; at threshold 1, grade 1 is admitted with a Lean bridge obligation to a source-facing S0 .
Relation
Interpretation
Grade
same
Same mathematical content and structure
3
trivial_equivalent
Immediate equivalence after notation or checked definitions
2
mutated_*
Substantive change supported by a bounded equivalence or directional proof
1
unaligned
Unsupported, mismatched, unresolved, or requiring a complex comparison
0
Table 1: Local semantic relations. The mutated_* family includes equivalent, stronger, and weaker changes; one-way changes are admissible only in the appropriate logical polarity.
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
Table 2: Controlled comparison on FormalTCS (143 items; one output per item).
Recall ↑
Missed errors ↓
Precision ↑
False alarms ↓
Accuracy ↑
Original labels
Direct judge
0.820
27
0.939
8
0.883
Fyan judge
0.873
19
0.771
39
0.807
Verified labels
Direct judge
0.636
75
1.000
0
0.750
Fyan judge
0.777
46
0.941
10
0.813
Table 3: Detecting inconsistent statements on ConsistencyCheck (300 items; inconsistent is the positive class). Missed errors are inconsistent statements judged consistent. The verified labels come from re-verifying all 300 statements against a single criterion (Section 3.3 ): 56 statements that the original labels call consistent become inconsistent, and none moves the other way. Bold marks the better method in each column; shaded rows are the Fyan judge. Confusion counts, F1, and bootstrap intervals are in Appendix B.3 .
Figure 3: Errors on ConsistencyCheck under the original and the verified labels (Table 3 ). The Fyan judge’s false alarms are split by grade; unknown marks runs without a valid record.
Case
Yardstick
Audit record (abridged)
Grade
(a) Arithmetic series (miniF2F)
Direct judge: consistent Experts: inconsistent
∑ k in range 5, a + k * d = 70 parses as (∑ka)+kd with a free k . Hypothesis slot ( − ), unaligned : “ 5a+kd=70 constrains a different object; a=28 , kd=−70 satisfies the candidate’s hypotheses but not the source.”
0 → repair
(b) Floor equation (miniF2F)
Experts: consistent Direct judge: consistent
Source: a=p/q with p,q relatively prime positive integers. Binder slot a : Q ( − ) also admits a≤0 : mutated_weaker , so at negative polarity “the candidate statement implies the source statement (a proof transfers), but it says something else”; repair: restrict a to the positive rationals.
1 → repair or bridge
(c) Product measure bounds (FormalTCS)
BEq + : not_proven
Every row names its conversion: n≥2 as n : N , n≥2 (condition moved into a type); D1,…,Dn as Fin n → ProbabilityMeasure R (reindexing); the product law as productLaw (Mathlib vs. local definition); both bounds same or reindexed. Premise: a division relies on Lean’s total division, as the text never excludes zero.
2 → accept
Table 4: One audit, three yardsticks (real records, abridged). Each yardstick returns one bit; the audit localizes the difference, grades it, and routes the statement. Relations and quoted arguments come from the Fyan Judge; polarity and grades are computed by code, and ( − ) marks negative polarity. Case (a) is from the diagnostic pool, not the evaluation sample.
Measure
Result
Formalized theorem units
20
Replaying under the current environment
17
Requiring library porting
3
Lean artifact
9,355 lines; 34 theorems; 118 lemmas
Table 5: ODENumLib at the document level. A unit is formalized when it contains no sorry and introduces no new axioms in its original environment. Replay is measured under the currently pinned Lean and Mathlib revisions.
Appendix figures & tables10 assets
Supplementary material from the paper’s appendix.
Appendix
Setting
Configuration
Model
DeepSeek-V4.1-Flash ( deepseek-flash )
Sampling
T2NP: T=0 , top- p=1 ; NT2FT and FT2FP: T=0.6 , top- p=0.9 ; one candidate per item, submitted once to the grader; no resampling
Released benchmark graders: BEq + for NT2FT, the FormalTCS Qwen3.8-Max rubric for T2NP, and strict Lean verification for FT2FP
Control
General-purpose agent using the benchmark prompts verbatim
Fyan
Reasoner for T2NP and the Formalizer for NT2FT/FT2FP, with the benchmark brief and stage preamble
Appendix
Table 6: FormalTCS experimental configuration. Shared settings apply to both the control and Fyan .
Method
TP
FN
TN
FP
No verdict
Accuracy
F1
Original labels
Direct judge
123
27
142
8
0
0.883 [0.847–0.917]
0.875
Fyan judge
131
19
111
39
10
0.807 [0.760–0.850]
0.819
Verified labels
Direct judge
131
75
94
0
0
0.750 [0.700–0.797]
0.777
Fyan judge
160
46
84
10
10
0.813 [0.767–0.853]
0.851
Appendix
Table 7: ConsistencyCheck confusion counts and aggregate metrics under the original and the verified labels (Section 3.3 ). “Inconsistent” is the positive class. Invalid or missing verdicts of the Fyan judge are treated as predictions of inconsistency and are already included in TP or FP; “No verdict” reports this diagnostic subset rather than an additional outcome category. Brackets give 95% bootstrap intervals.
Claim
Reference
Candidate
Reason for failure
Expected number of cycles
average using Lean’s total division
explicit zero branch for an empty family
equivalence requires a case split outside the tactic ladder
ReLU networks
inductive representation over affine maps
inductive representation over matrices and biases
independently declared representations cannot be identified
Best loss in a hypothesis class
bounded infimum whose empty fibers contribute zero
infimum over the image of the class
the reference does not encode the source infimum faithfully
Appendix
Table 8: Representative FormalTCS candidates reported as not_proven by BEq + . Lean code is abridged.
Unit
Lines
Statement
Current
Main result
exponential_bounds
111
≈
pass
product–exponential bound
taylor/remainder
186
≈
pass
Taylor remainder
ode
62
Δ
pass
local existence and uniqueness
gronwall/constant
162
=
pass
constant-coefficient discrete Grönwall
gronwall/variable
223
=
pass
variable-coefficient discrete Grönwall
taylor/lagrange
637
Δ
port
interpolation error
Appendix
Table 9: ODENumLib unit inventory and replay status under the pinned Lean/Mathlib environment.
Field
Purpose
source_graph , candidate
Reviewed source tree and the host-extracted Lean tree.
source_slots , candidate_slots
Binder, hypothesis, and goal slots cut by the host from each tree.
scope , polarity
Logical position of each slot and the binders or premises available to it, computed by the host.
Local relation of a group of paired slots or used definitions; the named conversion, argument, or concrete difference supporting it; and an optional repair .
affects , omissions
Downstream effects of changed objects, and unpaired slots, which the host scores as omissions.
checks , transfer
Required semantic checks and, when needed, object, hypothesis, and claim transfer evidence.
Appendix
Table 10: Principal fields of the semantic evidence record.
Relation
Evidence level
Interpretation
same
none
Same mathematical content and structure, up to consistent renaming.
trivial_equivalent
immediate
Immediate equivalence after notation or checked definitions are expanded.
mutated_equivalent
bounded local proof
Substantive reformulation with evidence in both directions.
mutated_stronger
bounded local proof
Candidate implies source.
mutated_weaker
bounded local proof
Source implies candidate.
mutated
bounded local evidence
Substantive object or representation change whose effects are tracked downstream.
Appendix
Table 11: Local semantic relations and their evidence requirements.
Binder
Sign
Adapter
Required body transfer
∀
+
d:U→V
Q(d(u))→P(u)
∀
−
d:V→U
P(d(v))→Q(v)
∃
+
d:V→U
Q(v)→P(d(v))
∃
−
d:U→V
P(u)→Q(d(u))
Appendix
Table 12: Direction-sensitive adapters for changed quantifier domains.
Component
May influence
Cannot determine directly
Specifier models
theorem grouping, candidate dependencies, generated unit text
graph validity, deterministic provenance, final downstream semantic acceptance
Lean verifies that a generated declaration is well typed, but not that it expresses the statement a user intended. We study two questions for autoformalization without canonical Lean targets: whether LLM judges can provide a usable proxy for human semantic review, and how much compilation overstates faithfulness across systems. Our criterion combines Lean compilation with strict semantic consensus between GPT-5.2 and Gemini-2.5-Pro. On an independently audited random sample, it agrees with human majority on 89.7% of cases (Wilson 95% CI: 82.1--94.3%). Across eight systems evaluated on 400 graduate-level statements, every system has a nonzero compile--faithfulness gap, whose observed magnitude ranges from 3.0 to 29.0 percentage points. The full GPT-5.2 tool-augmented agent shows the largest gap, compiling 89.5% while satisfying the semantic criterion on 60.5%. Human review, an independent third-family judge, and a BEq formal cross-check provide complementary evidence that the accepted core is reliable and that most audited outputs in the gap are genuine semantic mismatches. A secondary 23 factorial analysis shows that elaboration feedback is the largest validity intervention, yet does not eliminate semantic drift. LLM judging is therefore useful as a human-calibrated, conservative aggregate measure, not as an equivalence oracle.
Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy +3
University of California, Riverside · University of Arizona · University of California, San Diego
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 training data are scarce, and leading agents often rely on costly frontier models and manually engineered harnesses. To address the above issues, we present AIProver, an agentic framework for autonomous proof auto-formalization and proof synthesis (AFPS) that jointly post-trains a 119B open-weight language model and evolves its agentic, tool-calling harness with HarnessEvolve. Verifiers assess type correctness, proof completeness, and semantic correctness, returning rewards and diagnostic certificates that drive model fine-tuning and alternating reinforcement learning via symbolic feedback and HarnessEvolve, a certificate-driven evolutionary search over the whole harness control flow that re-tailors the harness to the updated model. For research-level training and evaluation, we introduce LoCoBench, 58.9k instances from Mathlib, CSLib, Mizar Math Library, and a bounded-arithmetic textbook, with a 771-instance validation split whose theorem-proof pairs have no public Lean formalization. Against 39 frameworks spanning AFPS agents, frontier LLMs, and coding agents, AIProver lifts pass@4 semantic correctness over its Leanstral-1.5 base from 15.7% to 36.7% and outperforms every other open-weight system and Aristotle. As a Claude Code and Codex skill, it lifts their semantic correctness from 41.9% and 34.1% to 79.8% and 62.4%, respectively. Further, it is also 24% cheaper than Numina-Lean-Agent, pushing the accuracy-cost frontier of research-level AFPS.
Prithwish Jana, Viet Bach Hoang, Logan Luna +9
Georgia Institute of Technology, USA · University of Pennsylvania, USA · Foothill College, USA +3
Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@k and refine@k metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of <\0.01$ per correct proof.
Tyson Klingner, Drew Bladek, Escher Crawford +6
Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA