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.AISep 30, 2026

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

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.

Figures & tables

Panel of Figure 1 — 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.

Panel of Figure 2 — 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 $S_{1}$ , with a grade $s_{i}$ per paired group. Code derives polarity, checks the record, and routes $S_{1}$ by the statement grade $\min_{i}s_{i}$ : 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 $S_{0}$ .

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 $\uparrow$	Missed errors $\downarrow$	Precision $\uparrow$	False alarms $\downarrow$	Accuracy $\uparrow$
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 .

Panel of Figure 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	$\sum$ k in range 5, a + k * d = 70 parses as $(\sum_{k}a)+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 $\rightarrow$ repair
(b) Floor equation (miniF2F)	Experts: consistent Direct judge: consistent	Source: $a=p/q$ with $p,q$ relatively prime positive integers. Binder slot a : $\mathbb{Q}$ ( $-$ ) also admits $a\leq 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 $\rightarrow$ repair or bridge
(c) Product measure bounds (FormalTCS)	BEq + : not_proven	Every row names its conversion: $n\geq 2$ as n : $\mathbb{N}$ , $n\geq 2$ (condition moved into a type); $D_{1},\dots,D_{n}$ as Fin n $\to$ ProbabilityMeasure $\mathbb{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 $\rightarrow$ 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
Lean	Lean 4.32.2; Mathlib revision 905b958 ; prebuilt cache unchanged
Graders	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	$\approx$	pass	product–exponential bound
taylor/remainder	186	$\approx$	pass	Taylor remainder
ode	62	$\Delta$	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	$\Delta$	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.
relation , conversion , argument , difference , evidence	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
$\forall$	$+$	$d:U\to V$	$Q(d(u))\to P(u)$
$\forall$	$-$	$d:V\to U$	$P(d(v))\to Q(v)$
$\exists$	$+$	$d:V\to U$	$Q(v)\to P(d(v))$
$\exists$	$-$	$d:U\to V$	$P(u)\to 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
Reasoner / Planner	proof strategy, lemma decomposition, candidate scaffold	final protected theorem interface or proof completion
Formalizer agents	proof plans, helper lemmas, executable proof search	completion state, protected signatures, axiom acceptance
Fyan Judge	structured comparison evidence	deterministic record validity or Lean proof validity
Curator	retrieved proof patterns and search suggestions	whether a resulting proof is accepted
Orchestrator / human	strategic advice, questions, critic activation	executable Lean, protected statements, or completion

Appendix

Table 13: Principal trust boundaries in the Fyan pipeline.

Setting	Default
Maximum proving iterations	50
Maximum concurrent provers, including nested subagents	4
Maximum dispatched objectives per iteration	10
Block execution on incomplete dependencies	true
Semantic protection	enabled
Faithfulness threshold	trivial

Appendix

Table 14: Principal Formalizer and semantic-audit defaults.

Setting	Default
Specifier maximum units generated per call	6
Specifier maximum prior-context budget	6,000 tokens
Specifier maximum verification revisions	2
Specifier maximum units repaired in validation	10
Maximum unit TeX size admitted to validation	40,000 characters
Curator promotion threshold	3 projects

Appendix

Table 15: Principal Specifier and Curator defaults.

Explore similar work

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
Jun 30, 2026Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy +3Theorem Proving Explanation Faithfulness
University of California, Riverside · University of Arizona · University of California, San Diego
AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness
Oct 4, 2026Prithwish Jana, Viet Bach Hoang, Logan Luna +9Theorem Proving
Georgia Institute of Technology, USA · University of Pennsylvania, USA · Foothill College, USA +3
Evaluation of LLMs for Mathematical Formalization in Lean
Jun 4, 2026Tyson Klingner, Drew Bladek, Escher Crawford +6Theorem Proving Formalization
Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA

Jun 30, 2026, cs.AIJ/K move · Enter open · S save

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie+2

University of California, Riverside · University of Arizona · University of California, San Diego

Theorem Proving Explanation Faithfulness Large Language Model Reliability

Open paper AskPDF arXiv

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

2^3

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.

Abstract

Explore similar work

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

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

Evaluation of LLMs for Mathematical Formalization in Lean