PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2609.39228v1cs.AI

TL;DR

Document-level formalization must coordinate interdependent theorems, and machine-checked proofs do not by themselves establish that statements preserve their sources. FYAN combines dependency-aware formalization with evidence-grounded semantic auditing and proof-transfer obligations for admitted changes. It reports more FormalTCS theorems proved than a general agent harness, a higher natural-language proof score, and higher audit recall than a direct LLM judge on original labels.

  • Problem

    Document-level formalization must identify theorem units, recover dependencies, order and reuse results, while formal correctness alone does not establish semantic faithfulness.

    Source: §1 · pp. 1–2

  • Method

    FYAN formalizes dependency-aware theorem units and uses validated evidence to govern stage advancement, with proof-transfer obligations for accepted substantive changes.

    Source: §1 · p. 2, §2.1 · p. 3, §2.3 · p. 5

  • Results

    86 of 143 FormalTCS theorems were proved under a strict Lean check versus 69 for a general agent harness, the natural-language proof score rose from 0.501 to 0.851, and audit recall on original labels was 0.827 versus 0.820.

    Source: §3.3 · p. 7, §4 · p. 9

  • Takeaways & Limitations

    For libraries whose results become dependencies, reproducible acceptance and Lean-checked bridges make accepted deviations depend on formal evidence rather than the judge's natural-language evidence alone.

    Source: §2.3 · p. 5, §4 · p. 10

    The evaluation uses one model and one trajectory per item, ODENumLib covers a single domain, and the audit costs more per statement than a single judgment.

    Source: §4 · p. 10

Abstract

from arXiv · show

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.

1 INTRODUCTION

Document-level formalization requires coordinating interdependent theorems, while preserving the meaning of each statement matters because errors can propagate through dependencies. FYAN addresses both challenges with a dependency-aware workflow and an evidence-grounded semantic audit.

1 INTRODUCTION

  • Document-level formalization must identify theorem units, recover dependencies, choose a valid order, reuse results, and maintain a coherent formal project.These requirements make scaling from isolated theorems to a mathematical document a substantially different problem.Source: §1 · p. 1
  • An accepted misformalization can become a dependency for later results, allowing semantic mismatches to propagate through a formally verified project.A proof assistant checks the theorem's formal correctness, not whether its statement faithfully represents the source.Source: §1 · p. 2
  • Existing alignment methods provide theorem-level signals, but document-level workflows also need decisions about advancement, justified deviations, and evidence for safe reuse.The cited approaches include provability, learned or prompted judgments, structural comparisons, expert references, and targeted consistency checks (Zhang et al., 2026a; Han et al., 2026; Ammanamanchi et al., 2026).Source: §1 · p. 2
  • FYAN decomposes sources into dependency-aware theorem units, formalizes them in dependency order, reuses proved results, and audits statements before proof search.Models and human experts can guide the workflow, but do not directly decide whether a theorem may advance.Source: §1 · p. 2
  • 86 of 143 FormalTCS theorems were proved under a strict Lean check, versus 69 for a general agent harness, while the natural-language proof score rose from 0.501 to 0.851.The same-model evaluation also reports higher audit recall than a direct LLM judge on ConsistencyCheck: 0.777 vs. 0.636 on verified labels and 0.873 vs. 0.820 on original labels; FYAN built ODENumLib with 20 dependency-linked theorem units and 9,355 lines of Lean.Source: §1 · p. 2

2 METHOD

FYAN organizes formalization around persistent project artifacts and dependency-aware control, while deterministic gates govern statement acceptance and proof completion. Its semantic audit records local source-to-Lean correspondences and uses polarity-aware checks; substantive admitted changes require a proof-transfer obligation.

2 METHOD

  • FYAN maps source documents into a provenance-tracked Lean project whose components communicate through persistent artifacts and explicit control boundaries.Models and experts may reason and guide, while validated evidence determines stage advancement and acceptance.Source: §2 · p. 2, §2.1 · p. 3

2.1 WORKFLOW AND CONTROL BOUNDARIES

  • The ORCHESTRATOR follows the document dependency DAG, schedules ready theorems, and makes proved upstream modules available to downstream proofs.REASONER and PLANNER prepare a natural-language proof, lemma-level plan, and compiling statement scaffold; FORMALIZER constructs proofs, while CURATOR skills may guide runs without counting as proof evidence.Source: §2.1 · p. 3, Figure 1 · p. 3
  • Human guidance and reusable skills are advisory, while persisted artifacts and a sole-writer gateway separate proof assistance from validated stage acceptance.The ORCHESTRATOR also cross-checks ongoing proofs against the argument, specification, and plan.Source: §2.1 · p. 3, Figure 1 · p. 3

2.2 EVIDENCE-GROUNDED SEMANTIC AUDITING

  • The audit pairs source and Lean slots for objects, hypotheses, claims, and definitions, recording local relations, scope, polarity, and omissions.The LLM proposes structured evidence, while deterministic checks assess coverage, admissibility, scope, dependencies, and evidence thresholds; a non-compensatory minimum grade governs the statement.Source: §2.2 · p. 4

2.3 PROOF TRANSFER AND BRIDGE OBLIGATIONS

  • A proof-transfer obligation connects an audited candidate statement S1 to a source-facing statement S0 through object, hypothesis, and claim transfer.For the covered logical fragment, scope-aware local certificates can compose into global transfer maps when coverage, scope, and witness dependencies are preserved; the bridge certifies only S1 → S0, not whether S0 faithfully represents the source.Source: §2.3 · pp. 5–6
  • By default, grades 2 and 3 are accepted directly and grade 1 returns for repair; lowering the threshold admits grade 1 with a Lean bridge obligation.The bridge must be discharged in Lean and is itself re-audited before being frozen.Source: §2.3 · pp. 5–6

3 EVALUATION

The evaluation tests FYAN on staged theorem formalization, semantic auditing, and document-level library construction. It reports gains in verified proof construction and auditing under specified comparisons, alongside a dependency-linked ODE formalization.

3.1 EXPERIMENTAL SETUP

  • The evaluation compares FYAN with a general-purpose harness on three FormalTCS stages using the same model, Lean environment, and graders, and assesses auditing on 300 balanced ConsistencyCheck items.ODENumLib is the document-level evaluation, with dependency-linked units that reuse proved upstream results.Source: §3.1 · p. 6

3.2 VERIFIED PROOF PRODUCTION

  • FYAN improves formal proof construction and natural-language reasoning over the general-purpose harness on FormalTCS, while NT2FT scores remain low for both systems.BEq+ requires close equivalence to the reference and does not identify independently declared types; the benchmark authors’ strongest reported result was 11.2% with Claude Opus 5 and eight samples per item.Source: §3.2 · p. 6, Table 2 · p. 6

3.3 SEMANTIC AUDITING FOR FAITHFULNESS

  • The audit leads on original-label recall, reporting 0.827 against 0.820, and localizes rejected mismatches to source objects, hypotheses, claims, or scope.Among 22 items only the audit classifies correctly, six are structural errors in scope, quantification, or intervals.Source: §3.3 · p. 7
  • Under verified labels, the audit leads on recall and accuracy, with false alarms falling from 39 to 10; the direct judge accepts 48 of 56 relabelled statements, while the audit rejects 29.The verified labels reclassify 56 statements as inconsistent; none moves in the other direction.Source: Table 3 · p. 7, §3.3 · p. 8

3.4 DOCUMENT-LEVEL FORMALIZATION

  • ODENumLib formalizes 20 dependency-linked units covering discrete Grönwall inequalities, remainders, local existence and uniqueness, and standard-solver error analysis.Substantial units include θ-method error bounds and consistency conditions for linear multistep methods.Source: §3.4 · p. 9, Table 5 · p. 9

4 CONCLUSION AND LIMITATIONS

FYAN combines document-level formalization with semantic auditing and deterministic acceptance decisions. The conclusion reports stronger FormalTCS results than a general agent harness, while noting limits in evaluation breadth, domain coverage, and audit cost.

4 CONCLUSION AND LIMITATIONS

  • With the same model, FYAN proves 86 of 143 FormalTCS theorems under strict Lean check against 69 for a general agent harness, and raises the natural-language proof score from 0.501 to 0.851.The conclusion also reports that the semantic audit catches more inconsistent statements than a direct judge under original and verified labels.Source: §4 · pp. 9–10
  • FYAN separates proof capability, semantic faithfulness, and formal correctness by letting models and experts guide while deterministic gates decide what enters the library.For library reliability, the authors contrast an extra repair round after a false alarm with silent downstream damage from an accepted misformalization.Source: §4 · pp. 9–10
  • The evaluation uses one model and one trajectory per item, ODENumLib covers one domain, and the audit costs more per statement than a single judgment.The authors identify broader model and domain evaluation, supervision ablations, and more mechanically checked Judge conversions as future work.Source: §4 · p. 10

AI USE STATEMENT

  • The paper reports generative AI use in system experiments and research tasks, with authors reviewing AI-assisted mathematical arguments, code, and manuscript content.The authors take responsibility for the final content, claims, and artifacts.Source: AI USE STATEMENT · p. 11

ETHICS STATEMENT

  • The work reports no human subjects or private or sensitive personal data, and describes permission scoping and isolated, low-privilege execution to address tool-related risks.Public benchmark data are used under their licenses, and the case-study source material is open.Source: ETHICS STATEMENT · p. 11

REPRODUCIBILITY STATEMENT

  • Appendices B–G provide evaluation protocols, audit analyses, the ODENumLib inventory, validation and transfer details, implementation boundaries, and configuration procedures.The reproducibility statement says the repository includes implementation, prompts, configurations, and supporting artifacts for reproducing the experiments.Source: REPRODUCIBILITY STATEMENT · p. 11, B EXPERIMENTAL DETAILS · p. 15

A RELATED WORK

  • Related work spans mathematical reasoning, semantic-faithfulness evaluation, and document-level harnesses; FYAN combines auditing, checked transfer obligations, and deterministic acceptance conditions.The FormalTCS protocol separately evaluates statement translation, natural-language proof generation, and Lean proof construction so errors do not propagate across stages.Source: A RELATED WORK · p. 15, §B.1 · p. 15

B.2 PROOFNET#

The appendix reports a standalone ProofNet# proof-engine evaluation and additional ConsistencyCheck accounting. It specifies strict solve criteria and describes the audit’s cost and disagreement patterns.

B.2 PROOFNET#

  • The proof engine solves 216 of 343 ProofNet# statements (63.0%) under strict criteria requiring compilation, declaration preservation, no sorry or new axiom, and a transitive axiom audit.The remaining outcomes are 109 proof failures, seven changed signatures, two compile failures, and nine infrastructure failures.Source: §B.2 · p. 16
  • Published ProofNet results are not used as a numerical baseline because they use a different Lean port and substantially larger Pass@N budgets.The reported evaluation includes 343 statements that elaborate in the pinned Lean environment; the FORMALIZER runs one trajectory with at most five prover iterations per theorem.Source: §B.2 · pp. 15–16

B.3 CONSISTENCYCHECK

  • ConsistencyCheck begins with 859 informal–formal pairs and retains 835 eligible items after library-drift and definition exclusions; the reported sample is 300 balanced labelled pairs.The audit uses extraction, local alignment, and deterministic validation; the direct baseline makes a single judgment with the same model and per-call settings.Source: §B.3 · p. 16
  • On the 300-item ConsistencyCheck evaluation, the audit is correct alone on 43 items under verified labels, versus 24 for the direct judge, but costs about 0.15 CNY per item against 0.007 CNY.Under original labels the corresponding alone-correct counts are 22 for the audit and 45 for the direct judge; 18 of 39 audit false alarms are grade 1.Source: §B.3 · p. 16

C ADDITIONAL SEMANTIC-AUDIT ANALYSIS

Appendix C outlines further analysis of reference-based equivalence, ConsistencyCheck disagreements, and semantic mismatches. Its table reports confusion counts and aggregate metrics under two label sets.

C ADDITIONAL SEMANTIC-AUDIT ANALYSIS

C.1 LIMITS OF REFERENCE-BASED EQUIVALENCE

The BEq+ grader can reject semantically reasonable candidates because it elaborates references and candidates separately and does not automatically identify independently declared types. Its scores therefore provide a complementary signal, not a definitive measure of semantic faithfulness.

C.1 LIMITS OF REFERENCE-BASED EQUIVALENCE

  • 91 of 143 FormalTCS references introduce a structure, inductive, or class, while all 5 control-harness BEq+ successes fall among the other 52 items (random-placement probability 0.0056).The grader shares only the longest verbatim common prefix between separately elaborated declarations.Source: §C.1 · p. 17
  • Table 8 presents three cases where BEq+ reports semantically reasonable candidates as not proven against the benchmark reference.The table gives representative cases, with Lean code abridged.Source: Table 8 · p. 17, §C.1 · p. 17
  • A failed equivalence proof need not imply a semantic mismatch, and a benchmark reference need not be a perfect semantic ground truth.A separate Lean proof establishes equivalence in one example; another reference admits an unintended zero contribution outside the intended class.Source: §C.1 · p. 17

C.2 CONSISTENCYCHECK ERROR ANALYSIS

The ConsistencyCheck analysis distinguishes audit false alarms from label errors and tests the consequences of acceptance thresholds and missing verdicts. Re-verification supports the audit’s higher recall, while boundary cases show why unresolved statements are returned rather than accepted automatically.

C.2 CONSISTENCYCHECK ERROR ANALYSIS

  • 29 of the audit’s 39 apparent false alarms were not the text’s statement, leaving 10 false alarms attributable to the audit itself.The 29 comprise 13 grade-1 reports, 14 grade-0 rejections, and 2 runs without a valid record.Source: §C.2 · pp. 17–18
  • Lowering direct acceptance to grade 1 would reduce recall from 0.873 to 0.653 (98/150) while raising precision to 0.824 under the original labels.The audit therefore keeps grade 2 as its direct-acceptance threshold and requires a Lean-checked bridge for grade-1 statements.Source: §C.2 · p. 18
  • On verified labels, the FYAN judge reaches recall 0.777 and F1 0.851, versus 0.636 and 0.777 for the direct judge, respectively.All 300 statements were screened blind to original labels and method predictions, with every class confirmed by the authors.Source: §C.2 · pp. 18–19
  • All 10 runs without a verdict end in rejection after three consecutive failures to produce a record that passes validation.Excluding them gives recall 0.867 (124/143) and precision 0.775; counting them as acceptances gives recall 0.827 (124/150), versus 0.820 (123/150) for the direct judge.Source: §C.2 · p. 18
  • Two of three expert-consistent boundary cases require context or an extension argument that is not explicit in the formal statement.For the finite-dimensionality example, the validator refuses to accept context outside the statement; the recurrence example requires an extension argument across changed indexing.Source: §C.2 · p. 18
  • Grades 2 and 3 indicate alignment up to trivial equivalence, grade 1 marks a substantive but potentially recoverable change, and grade 0 marks an unsupported mismatch.A grade-1 statement requires proof transfer rather than acceptance based only on mathematical plausibility.Source: §C.2 · p. 19

C.3 REPRESENTATIVE SEMANTIC FAILURE CASES

The examples show that plausible, compilable Lean statements can still differ semantically from their sources through scope or definition choices. In one case the audit localizes the missing summand; in another, Lean’s meaning of “ideal” differs from the source’s.

C.3 REPRESENTATIVE SEMANTIC FAILURE CASES

  • A misplaced delimiter moves the common-difference term outside the summation, so the candidate constrains different objects despite remaining syntactically plausible.The direct judge accepts the statement, while the FYAN judge rejects affected hypothesis rows and localizes the missing occurrence of the term.Source: §C.3 · p. 19
  • For the matrix-ring example, the source uses a two-sided ideal, whereas Lean’s Ideal denotes a left ideal over a noncommutative semiring.The stated conclusion holds under the source notion but not under Lean’s notion.Source: §C.3 · p. 19
  • The judgment accepted a semantically different object despite available Mathlib evidence, because the comparison did not require checking whether the formal and source notions of “ideal” matched.The example identifies a limitation of retrieval alone: relevant evidence may not affect a verdict without an explicit comparison.Source: §C.3 · p. 19

D ODENUMLIB CASE STUDY

ODENumLib is a dependency-linked Lean development generated from numerical-analysis lecture notes, but it was built before FYAN’s semantic audit. Its replay status and statement changes show why project completion and theorem-file closure should be distinguished from faithful, reusable formalization.

D ODENUMLIB CASE STUDY

  • ODENumLib contains 23 theorem units spanning discrete Grönwall inequalities, Taylor and interpolation remainders, convergence, and stability of standard ODE solvers.Table 9 provides the unit inventory and replay status under the pinned Lean/Mathlib environment.Source: D ODENUMLIB CASE STUDY · p. 19, Table 9 · p. 20
  • 20 of 23 units closed without sorry or newly introduced axioms in the original environment, but only 17 replay directly under the pinned environment.Three previously closed units require porting because of library-level type changes, and three units remain open.Source: D ODENUMLIB CASE STUDY · p. 19
  • Nine of the 19 units with retained pre-proof scaffolds undergo a substantive change to the main statement.Some changes repair inadequate scaffolds, while others weaken or ease the final theorem relative to the source-facing result.Source: D ODENUMLIB CASE STUDY · pp. 19–20
  • The runge kutta 4 scaffold already assumes the local truncation estimate the source result is intended to derive, while convergence/dahlquist proves only one direction of the stated result.Project completion cannot be assessed solely by whether files close, because substantive statement changes become interfaces for downstream units.Source: D ODENUMLIB CASE STUDY · p. 20

E SEMANTIC AUDIT AND PROOF TRANSFER: TECHNICAL DETAILS

The semantic audit pairs model-constructed local evidence with deterministic validation to assess source–Lean alignment. Its records preserve omissions, scope, polarity, and transfer requirements rather than relying on a free-form verdict.

E SEMANTIC AUDIT AND PROOF TRANSFER: TECHNICAL DETAILS

  • The FYAN Judge builds localized evidence between the source and candidate Lean statement, while deterministic code validates its structure, coverage, logical direction, and consistency.Accepted substantive deviations also require transfer obligations for object coverage, hypothesis transfer, and claim transfer.Source: E SEMANTIC AUDIT AND PROOF TRANSFER:… · p. 20, §E.1 · p. 22

E.1 STRUCTURED EVIDENCE AND DETERMINISTIC VALIDATION

  • A source-first comparison pairs slots from reviewed source and elaborated Lean trees; unmatched slots remain visible as omissions, and many-to-many correspondences are allowed.Types, subtypes, instances, implicit parameters, and definitions can encode mathematical content whose downstream effects must be recorded when representations change.Source: §E.1 · pp. 20–21
  • Local relations specify the conversion required between corresponding items, with admissible direction determined by each item’s polarity in the complete theorem.A bounded local proof must use the source context, checked definitions, and identified conversion lemmas; an unestablished relation does not itself prove inequivalence.Source: §E.1 · pp. 21–22
  • Deterministic validation checks record structure, coverage, admissible relations, evidence, and consistency before non-compensatory aggregation assigns grades 3 through 0.Malformed records may receive form repair, but a valid unfavorable record is not resampled; grades are policy labels, not probabilities or truth values.Source: §E.1 · p. 22

E.2 FROM LOCAL EVIDENCE TO GLOBAL PROOF TRANSFER

Scope-aware local certificates can compose into a proof transformer from an audited candidate theorem to a source-facing statement. The appendix also specifies how omissions, changed domains, bridge obligations, and implementation checks constrain that transfer.

E.2 FROM LOCAL EVIDENCE TO GLOBAL PROOF TRANSFER

  • Given object, assumption, and conclusion maps e, a, and g, any proof of S1 yields a canonical proof transformer κ : S1 → S0, and such transfers compose.The maps adapt source objects and assumptions to the candidate theorem, then recover the source conclusion.Source: §E.2 · p. 22
  • Signed local comparisons request direction-sensitive certificates; polarity reverses in implication antecedents, and certificates must respect binder scope and witness dependencies.The construction composes certificates over logical structure but is sufficient rather than complete; larger enclosing expressions may require an explicit certificate.Source: §E.2 · pp. 23–24

E.3 OMISSIONS AND CHANGED DOMAINS

  • Omissions remain explicit and are modeled by replacing deleted conjuncts with ⊤ or deleted disjuncts with ⊥; changed quantifier domains require directionally appropriate witness adapters.Adapters may use variables already in scope, but not future witnesses; whether they preserve the intended representation remains a separate semantic question.Source: §E.3 · p. 24

E.4 BRIDGE OBLIGATIONS AND DETERMINISTIC COMPLETION

  • An accepted non-identical candidate is frozen and receives an explicit bridge obligation to a source-facing statement, which must be semantically reviewed and proved in Lean.Completion also requires a successful build, current certifications, discharged bridges, zero target-scope sorry count, and an acceptable transitive axiom audit.Source: §E.4 · pp. 24–25

E.5 EXECUTABLE FRAGMENT AND GUARANTEE BOUNDARY

  • The executable checker supports a sufficient logical fragment and verifies coverage, scope, polarity, and certificate direction, but it does not prove arbitrary model explanations true.General changed-domain witnesses must be supplied or justified by a larger certificate; successful symbolic recipes are not Lean terms or kernel verdicts.Source: §E.5 · p. 25
  • Proof transfer and semantic faithfulness remain separate: Lean checks the bridge from S1 to S0, while the audit remains responsible for whether S0 interprets the source correctly.The bridge does not establish that the source-facing statement is the correct interpretation of the natural-language source.Source: §E.5 · p. 26

F SYSTEM IMPLEMENTATION

  • The system implementation maintains provenance, dependency-aware execution, protected theorem interfaces, and advice-only interaction across the formalization project.The implementation description emphasizes boundaries affecting the paper’s claims; prompts, numerical defaults, and reproduction commands are collected separately.Source: F SYSTEM IMPLEMENTATION · p. 26

F.1 PROJECT CONSTRUCTION, PROVENANCE, AND SCHEDULING

  • The project builder organizes source statements into theorem units and a validated dependency DAG, then schedules units topologically so completed upstream modules can be reused.Provenance is stored with source file, page range, and anchor; deterministic checks validate unit coverage, dependencies, cycles, and layering.Source: §F.1 · pp. 26–27

F.2 REASONING, PLANNING, AND LEAN PROOF CONSTRUCTION

The proving pipeline separates model-proposed reasoning and search from deterministic control of protected artifacts and theorem acceptance. It also curates reusable proof experience and provides supervision and human guidance without granting either authority over acceptance.

F.2 REASONING, PLANNING, AND LEAN PROOF CONSTRUCTION

  • REASONER adapts proof generation to preserve provenance and reuse proved upstream theorems, while PLANNER creates a lemma-level dependency graph, Blueprint, and compiling statement scaffold.Candidate library lemmas are checked against the live Lean environment, and the scaffold freezes interfaces without weakening difficult conclusions.Source: §F.2 · p. 27
  • FORMALIZER runs autoformalization, proving, and polishing iterations in which agents propose objectives, prove them, and receive deterministic validation and review.The plan–prove–review structure is retained, but consequential state transitions are decided outside the model; Lean tools guide search without determining acceptance.Source: §F.2 · p. 27

F.3 PROTECTED ARTIFACTS AND DETERMINISTIC COMPLETION

  • An agent’s COMPLETE token is only a request; deterministic completion requires a successful current build, zero target-scope sorry count, intact certifications, discharged required bridges, and an acceptable axiom audit.Missing or stale evidence fails closed, and human-facing review prose does not override deterministic counts.Source: §F.3 · pp. 27–28

F.4 CURATED REUSE, SUPERVISION, AND HUMAN GUIDANCE

  • CURATOR turns completed runs into reusable proof and tactic patterns, but these model-generated skills guide search rather than count as proof evidence.The paper does not attribute an independent empirical effect to CURATOR.Source: §F.4 · p. 28
  • ORCHESTRATOR and human guidance can shape strategy through advice-only channels, but cannot edit protected statements, inject executable proof code, or bypass the completion gate.The paper does not evaluate ORCHESTRATOR supervision as an independent capability intervention.Source: §F.4 · p. 28

F.5 PIPELINE TRUST BOUNDARIES

  • The trust boundary lets model components expand candidate formalizations and proof searches while persisted evidence and deterministic checks govern which artifacts become reusable.The FYAN Judge receives only its audit input, and unavailable required evidence or protected state causes the corresponding check to fail closed.Source: §F.5 · p. 29

G REPRODUCIBILITY AND CONFIGURATION

Appendix G records FYAN’s workflow defaults, semantic-audit procedure, and reproduction requirements. It distinguishes configurable search and review settings from the checks required for theorem acceptance.

G REPRODUCIBILITY AND CONFIGURATION

  • Appendix G supplements evaluation protocols with workflow defaults and reproduction information.Its focus is the defaults governing the workflow, semantic audit, and document-level execution.Source: G REPRODUCIBILITY AND CONFIGURATION · p. 29

G.1 SYSTEM CONFIGURATION

  • Project settings can be overridden, but changing operational budgets does not bypass protected-artifact, build, bridge, or axiom checks.The default bridge policy requires a proof-transfer bridge for an admitted substantive deviation.Source: §G.1 · p. 29

G.2 PROMPTS AND SEMANTIC-AUDIT INPUT

  • Each semantic-audit stage uses a fresh model call with its own input, while invalid records receive bounded structural repair rather than repeated voting on valid unfavorable judgments.The audit inputs include the source text, reviewed source tree, candidate Lean tree, and host-computed slots.Source: §G.2 · pp. 29–31
  • The audit pairs source and Lean slots by relation, distinguishing equivalent encodings from changes in meaning or claim strength.Binders, hypotheses, and goals are compared in separate rows unless one side unpacks a single slot; unmatched slots are scored by the host.Source: §G.2 · p. 31
  • A separate meaning audit checks the original text for missing or extra conditions, conclusion scope, realized notions, domain effects, and non-vacuity.It records defects with a source quote and the corresponding Lean difference.Source: §G.2 · p. 32

G.3 REPRODUCTION RECORDS AND INDEPENDENT VERIFICATION

  • Reproduction records bind results to source, configuration, prompts, model settings, software revisions, logs, and independent verification; Lean checks include signatures, proof omissions, and transitive axioms.Semantic evidence and formal verification are retained separately, so reproducing only the final Lean file does not reproduce the full acceptance decision.Source: §G.3 · pp. 32–33
Loading 2609.39228v1…