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

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number, fraction and page or table reference, the quotations, the technique steps against Sections 2 and E to G, the Judge prompt lists and the Verus forms; corrected the model scope of the measurements, the trust list, a scaffold step the paper lacks, the criterion behind the re-verified labels, the ODENumLib scaffold inference and the threat paragraph; Verus keywords checked against Verus papers in the corpus.

source: Zhao, Zou, Ding, Wu, Wang, Mao, Zhang, Luo, arXiv:2609.39228v1 (30 Sep 2026), 33 pages with appendices A to G; http://arxiv.org/abs/2609.39228v1

what the paper is about, in one paragraph

Fyan turns a mathematical document (PDF, TeX or Markdown) into a Lean 4 project. Its subject is not proof search but the step before it: deciding whether a generated Lean statement says what the source says. The paper’s premise is “A proof assistant checks the theorem, not whether it faithfully represents the source.” (§1, p.2). Its answer is an audit in which a language model only fills in a structured comparison record and fixed code computes the verdict, plus a rule that any accepted difference must be backed by a Lean proof that the accepted statement implies a statement closer to the source. Everything below is Lean and mathematics in the paper; every Verus form is this study’s inference.

what is proved or measured, and what stays trusted

Proved on paper (Appendix E.2, pp.22-24): Proposition 1 (three maps e, a, g give a function from proofs of the candidate S1 to proofs of the source-facing S0), Lemma E.2 and Theorem E.1 (local certificates with the right direction compose into those maps). These are pen-and-paper proofs; the paper does not say they are mechanized.

Measured (FormalTCS and ConsistencyCheck with DeepSeek-V4.1-Flash and one output per item; the paper names no model for ProofNet# or ODENumLib):

• FormalTCS, 143 items, Table 2 (p.6): strict Lean pass on the proving task FT2FP 86/143 (60.1%) for Fyan against 69/143 (48.3%) for a general agent harness; natural-language proof rubric mean 0.851 against 0.501; statement translation certified equivalent by the BEq+ grader 8/143 (5.6%) against 5/143 (3.5%).
• ConsistencyCheck, 300 sampled items, 150 labelled consistent and 150 inconsistent, Table 3 (p.7) and Table 7 (p.17): numbers under technique 3 below.
• ProofNet#, the proof engine alone, at most five prover iterations: 216 of 343 statements (63.0%) (Appendix B.2, p.16).
• ODENumLib: 9,355 lines of Lean, 34 theorems, 118 lemmas (Table 5, p.9).

Trusted (the first two by the paper’s own account, the last two this study’s inference):

• the model’s free-text arguments inside the record. “In particular, deterministic validation can verify that required evidence is present, well-scoped, internally consistent, and used in the correct logical direction, but it cannot establish the truth of an arbitrary free-form mathematical explanation supplied by the model.” (Appendix E.5, p.25)
• that the source-facing statement S0 is itself the right reading of the text (next quote under technique 4)
• the extraction of the source tree, checked only by a second model call
• the Lean kernel, the pinned Mathlib and the configured axiom allow-list

technique 1: slot-paired semantic audit, source first

what it is: a comparison of an informal statement N with a formal candidate S1 in which both are cut into the same kinds of pieces (slots) by code, and the model’s only job is to say how each group of paired pieces relates.

when to use: between statement generation and proof search, for any statement that later work will import. The paper places it there because a wrong statement, once accepted, is silently reused (§1, p.2).

how it is done (§2.2, p.4; Appendix E.1, pp.20-22; Appendix G.2, pp.29-32):

1. extract a formula tree of the source before the model sees any formal text, each definition and atom anchored by a literal quotation; have a separate call review it. “Before any Lean is shown, one call extracts a formula tree of N whose definitions and atoms are anchored by literal source quotations, and an independent call reviews it.” (§2.2, p.4)
2. the host (code, not the model) reads the formal tree from the elaborated declaration together with the bodies of the definitions it reaches (§2.2, p.4)
3. the host cuts both trees into slots: binder domains (objects), hypothesis conjuncts, goal conjuncts, used definitions; it computes scope and polarity for each (§2.2, p.4)
4. the model writes one row per group of corresponding slots: relation, the named conversion or the argument or the concrete difference, and optionally a repair (Table 10, p.21). Binders, hypotheses and goals go in separate rows unless one side is a single slot the other unpacks (Judge prompt, p.31)
5. a slot that no row pairs is left out by the model and scored by the host. “Because both sides are cut into slots, source content that has disappeared entirely remains visible: it leaves a source slot that no row pairs, which the host scores as an omission.” (§2.2, p.4)
6. the model also fills a fixed checklist over the original text, in this order: hypotheses_present, no_extra_conditions, conclusion_strength, notions_realized, domains_types, non_vacuity (Judge prompt, p.32)
7. strip the candidate’s comments before the call. “Candidate-authored comments never reach the FYAN Judge, because they constitute neither source evidence nor instructions to the audit.” (Appendix E.1, p.20)

the paper’s example: the source assumes x > 0 and x < 1, the Lean statement has only x > 0; the first is paired, the slot for x < 1 stays unpaired and is recorded as an omitted hypothesis (§2.2, p.4).

two rules from the prompt worth copying verbatim into any such judge: “Choose the relation by what it takes to get from P to L, not by whether the theorem survives.” (Judge prompt, p.31); and a definition is compared by its body, not its name (same prompt, p.32, paraphrased here).

Verus form. Inference: for a Verus function the slots already exist syntactically. Binder slots are the parameters with their types (u64 against int or nat is a domain difference in the paper’s sense); hypothesis slots are the conjuncts of requires; goal slots are the conjuncts of ensures; definition slots are the spec fn bodies the contract mentions, to be read through to their bodies, including closed spec fn. Inference: the checklist carries over almost word for word: domains_types becomes overflow and nat subtraction, notions_realized becomes whether a spec fn is the notion the requirement names or an uninterpreted or trivially true one, non_vacuity becomes whether the requires is satisfiable and the ensures is more than ensures true. Inference: what does not carry over is the source side: a product requirement is rarely a single quantified formula, so step 1 is harder than for a textbook exercise, and the paper gives no evidence for prose requirements about programs.

evidence: technique 3.

where it fails: the paper’s own failure case is Herstein Exercise 4.3.25, where the text means a two-sided ideal and Lean’s Ideal over a noncommutative semiring is a left ideal; the record contained that fact and still accepted. “This example illustrates an important limitation of retrieval alone: relevant evidence may be available without affecting the verdict unless the audit explicitly requires the corresponding comparison.” (Appendix C.3, p.19)

technique 2: polarity decides which one-way changes are admissible

what it is: a rule, computed by code from the position of a slot in the whole formula, for whether a candidate piece that is stronger or weaker than the source piece can still yield the source statement.

when to use: whenever a formal statement differs from its source by a strengthening, a weakening, an omission or a changed quantifier domain.

how it is done (§2.2, p.4; Appendix E.1, p.22; Appendix E.3, p.24):

1. give the theorem root positive polarity; conjunction, disjunction and quantifier bodies keep the sign; negation and the left side of an implication flip it (Appendix E.2, p.23)
2. at a positive slot require candidate implies source; at a negative slot require source implies candidate. “Thus candidate conclusions may be stronger, while candidate assumptions may be weaker.” (§2.2, p.4)
3. a slot occurring at both polarities needs both directions (Appendix E.1, p.22)
4. treat an omission as a replacement and apply the same rule. “A deleted conjunct is represented locally by replacement with ⊤, while a deleted disjunct is represented by ⊥.” (Appendix E.1, p.22)
5. for a changed quantifier domain, require an adapter function in the direction Table 12 (p.24) gives: for a universal at positive polarity a map d from source domain U to candidate domain V with Q(d(u)) → P(u); universal negative, d : V → U with P(d(v)) → Q(v); existential positive, d : V → U with Q(v) → P(d(v)); existential negative, d : U → V with P(u) → Q(d(u)). “Adapters may depend on variables already in scope, but not on future witnesses.” (Appendix E.3, p.24)

the paper’s examples: replacing (A ∧ H) → G by A → G is recoverable, replacing A → (G ∧ H) by A → G is not (§2.2, p.4). The inclusion of the integers in the reals cannot carry ∃r ∈ R, 2r = 1 to ∃z ∈ Z, 2z = 1 (Appendix E.5, pp.25-26). Swapping ∀x ∃y to ∃y ∀x is not justified by local agreement (Appendix E.5, p.25).

Verus form. Inference: this is the ordinary rule for refining a contract. Suppose the requirement reads as requires A0, ensures G0 and the agent wrote requires A1, ensures G1. The agent’s contract serves the requirement when A0 implies A1 and G1 implies G0, so a dropped requires conjunct is admissible and a dropped ensures conjunct is not. Inference: polarity flips again inside an ensures of the form p ==> q: there the agent may weaken p and strengthen q, not the reverse. Inference: a changed domain needs the adapter too: a spec over nat offered for a requirement over int covers fewer inputs when the variable is an input (admissible only at a negative binder if the requirement really excludes negatives) and is a different claim when it is an output.

evidence: none separate; the rule is the content of Lemma E.2 and Theorem E.1 (pp.23-24).

where it fails: “The construction is sufficient rather than complete.” (Appendix E.2, p.24). The executable checker covers only ⊤, ⊥, conjunction, disjunction, implication and fixed-domain quantifiers, handles omissions only in the four explicit forms, and does not synthesize domain adapters (Appendix E.5, p.25).

technique 3: the model fills a record, code computes the grade

what it is: the verdict is the minimum of per-row grades, computed by a validator; the model may not author a score.

when to use: wherever a model’s judgment gates what enters a reusable library and the gate must be reproducible.

how it is done (§2.2, pp.4-5; Table 1, p.5; Table 11, p.21; Appendix E.1, p.22):

1. four relation families with fixed grades: same 3; trivial equivalent 2; mutated (equivalent, stronger, weaker, or a tracked representation change) 1; unaligned 0 (Table 1, p.5)
2. a grade-2 row must name its conversions from a closed list: bundling, currying, binder order, argument order, condition moved into a type, Mathlib vs local definition, inlining, implicit context, renaming, reindexing, standard unfolding (Judge prompt, p.31)
3. a grade-1 row must give a bounded local proof: a short derivation from the source context, checked definitions and identified conversion lemmas; reproving the theorem does not count (Appendix E.1, p.21)
4. code checks schema, identifiers, cross-references, that every slot is in a row or scored as an omission, that each relation is admissible at its polarity, that grade-2 rows name listed conversions, that no placeholder stands in for evidence (Appendix E.1, p.22)
5. statement grade = min over rows, omissions, required checks and transfers. “The minimum is non-compensatory: a single unresolved, unknown, or overly complex comparison cannot be offset by well-aligned items.” (§2.2, p.5)
6. route: grade 2 or 3 accept and freeze; below the threshold return to the formalizer with a localized repair request naming the item at fault, the direction of change and a suggested fix (Figure 2, p.4); at most 3 statement-repair attempts (Table 14, p.30)
7. a malformed record is repaired in form by the same judge against the unchanged inputs, up to 3 times per call; a well-formed unfavorable record stands. “Once a valid unfavorable record has been produced, it is not resampled merely to obtain a different judgment.” (Appendix E.1, p.22)
8. no valid record after three tries is a rejection (fail closed) (Appendix C.2, p.18)

Verus form. Inference: steps 1 to 8 are independent of the proof language; for VL the candidate side would be the function signature with requires and ensures and the reached spec fn bodies. Inference: the closed conversion list must be rewritten for Rust, since “Mathlib vs local definition” and “implicit context” have no Rust counterpart, while “condition moved into a type” does (a bound carried by u8 instead of a requires conjunct) and so does “standard unfolding” (a spec fn against its body).

evidence: ConsistencyCheck, 300 items sampled with a fixed seed from 835 eligible of 859, the direct judge and the audit both on DeepSeek-V4.1-Flash at low reasoning effort (Appendix B.3, p.16). Inconsistent is the positive class. Counts from Table 7 (p.17), checked against the rates in Table 3 (p.7):

• original labels: audit TP 131, FN 19, TN 111, FP 39, so recall 131/150 = 0.873, precision 131/170 = 0.771, accuracy 242/300 = 0.807; direct judge TP 123, FN 27, TN 142, FP 8, so recall 0.820, precision 123/131 = 0.939, accuracy 0.883
• labels re-verified by the authors (206 inconsistent, 94 consistent): audit 160/46/84/10, recall 160/206 = 0.777, precision 0.941, accuracy 0.813; direct judge 131/75/94/0, recall 0.636, precision 1.000, accuracy 0.750; exact McNemar p = 0.027 on 43 against 24 items where only one method is right (Appendix C.2, p.18)
• 10 of the audit’s 300 runs ended with no valid record and count as rejections; counted as acceptances instead, recall under the original labels is 124/150 = 0.827 against 0.820 (Appendix C.2, p.18)
• cost: about 0.15 CNY per item against 0.007 CNY for the direct judgment (Appendix B.3, p.16)

where it fails: on the original labels the audit is less accurate than the one-call judge (0.807 against 0.883) and its lead in recall nearly vanishes once the 10 no-verdict runs are not counted in its favour. Inference: its lead rests on the re-verified labels, which the authors produced themselves with Claude Opus 5.5 screening, under a criterion that the audit encodes in its conversion list and threshold but that the direct judge is also instructed to apply (§3.3, p.8; Appendix C.2, p.18). The misses are at one place: “Every one of the 46 inconsistencies that the audit misses is a grade-2 acceptance, in which the Judge recorded a difference as one of the listed conversions, and all 6 statements graded 3 are consistent.” (§3.3, p.8). Inference: 46 of 206 inconsistent statements passing means the closed conversion list, as applied by this model, is the weak point, and “standard unfolding” is the entry with the widest wording.

technique 4: bridge obligation for an accepted difference

what it is: when a grade-1 statement S1 is admitted, the system writes a source-facing statement S0 and requires a machine-checked proof of S1 → S0.

when to use: when the formal statement that is convenient to prove is not the statement the source makes, and one still wants the source’s statement.

how it is done (§2.3, pp.5-6; Appendix E.2, pp.22-23; Appendix E.4, pp.24-25):

1. write S0 := ∀x : X, A0(x) → G0(x) and S1 := ∀y : Y, A1(y) → G1(y)
2. the record supplies three pieces of evidence: object coverage e : X → Y; hypothesis transfer a : A0(x) → A1(e(x)); claim transfer g : A0(x) → G1(e(x)) → G0(x)
3. from a proof p of S1 the source proof is κ(p)(x)(h) = g x h (p (e x) (a x h)) (Equation 1, p.5)
4. by default a grade-1 statement is returned for repair; only if the threshold is lowered to 1 is S1 frozen with the obligation (§2.3, p.5)
5. the prover proves S1 without touching its frozen signature, then states theorem <root>_faithful : S0 and proves it from the frozen root (Appendix E.4, p.25)
6. S0 is itself audited against the source before it is frozen (Appendix E.4, p.25)

Verus form. Inference: for a proof fn, the bridge is a second proof fn whose requires is A0 and whose ensures is G0 and whose body calls the first; Verus then checks A0 implies A1 at the call and G1 implies G0 at the end, which are exactly a and g. For executable code it is a thin wrapper fn carrying the source-facing requires and ensures that calls the function with the convenient contract. Inference: the object map e is the argument expression at that call, for example a cast or a view of a concrete value as a Seq. Inference: what does not carry over is cost: in Lean the bridge is one more theorem, in Verus the wrapper is one more function in the public interface, so the frozen thing should be the wrapper’s contract.

evidence: none measured. The paper reports no count of bridges stated or discharged; ODENumLib predates the audit (see contradictions).

where it fails: “The bridge certifies only the formal implication S1 → S0 ; whether S0 faithfully represents the source remains the responsibility of the semantic audit in Section 2.2.” (§2.3, p.6). Lowering the threshold to 1 without bridges would, under the original labels, drop recall from 0.873 to 98/150 = 0.653 and raise precision to 0.824 (Appendix C.2, p.18).

technique 5: frozen signatures and a completion gate that asks no model

what it is: after the audit accepts a statement its normalized signature is bound to the source text, the local definitions and the evidence; completion is decided by code over six conditions.

when to use: in any loop where the agent that proves could also edit what is to be proved.

how it is done (Appendix E.4, pp.24-25; Appendix F.3, pp.27-28; Appendix G.3, p.32):

1. store the normalized signature with bindings to the source-facing input and the audit evidence
2. any later change to the signature or to a bound input invalidates the certification. “Subsequent changes to a protected signature or one of its bound inputs make the corresponding certification stale rather than silently transferring approval to the modified statement.” (Appendix E.4, p.24)
3. treat the agent’s claim of completion as a request. “An agent-generated COMPLETE token is therefore only a request.” (Appendix F.3, p.28)
4. the gate requires, per root: the count of sorry in the target scope is available and zero; the project builds; every frozen signature and its bound inputs are current; every bridge is discharged and its declaration still present; the root carries its semantic certification; a transitive axiom audit finds no sorryAx and no axiom outside the allow-list (Appendix E.4, p.25)
5. missing or stale evidence fails closed (Appendix F.3, p.28)
6. after generation an independent verifier recompiles each theorem, compares the declaration with the frozen signature, rejects sorry and admit, and audits transitive axioms (Appendix G.3, p.32)

Verus form. Inference: the same six conditions with Verus’s escape hatches in place of Lean’s: no assume, no admit(), no #[verifier::external_body] and no assume_specification outside an explicit allow-list; the crate verifies; the text of each frozen requires and ensures and of every spec fn it reaches is unchanged since the audit. Inference: “transitive” matters as much in Verus: an assume inside a proof fn three calls away from the root invalidates the root, so the scan must follow the call graph rather than the file under edit. Inference: Lean reports the axioms a theorem depends on through one command; the notes used for this study show no Verus counterpart, so this scan would be VL’s own code.

evidence: FT2FP in Table 2 is graded by exactly such a check (compilation, signature preservation, axiom checking, fresh kernel replay; §3.1, p.6). On ProofNet#, of 127 failures among 343, seven were changed signatures (Appendix B.2, p.16), that is 7/343 = 2.0% of items. Inference: these are runs in which the prover altered the statement it was given.

where it fails: the gate checks that the statement is unchanged, not that it was right; ODENumLib passed the gate with weakened statements (see contradictions).

technique 6: document cut into units with a graph checked by code

what it is: a model groups the source’s statements into theorem units and proposes dependencies; code validates the graph and recomputes the order.

when to use: when formalizing many interdependent results, so later ones import earlier proved ones.

how it is done (Appendix F.1, pp.26-27):

1. store every extracted statement with file, page range and anchor; provenance is inserted by code
2. a model groups statements into units and proposes edges, helped by a reference graph extracted from explicit cross-references
3. code checks the result. “In particular, deterministic validation requires every source statement to belong to exactly one unit, checks that dependency targets exist, rejects cycles, and recomputes the topological layering from the dependency relation rather than trusting a model-generated ordering.” (Appendix F.1, p.26)
4. each generated unit is compared with its source statements by a rubric (coverage, hypotheses, added assumptions, conclusions, dependencies) and by lints. “Independent deterministic lints detect selected high-risk changes, including lost biconditionals, altered strict inequalities, newly introduced asymptotic terms, malformed provenance, and undeclared cross-unit dependencies.” (Appendix F.1, p.26)
5. schedule units in topological order; a unit is ready only when all dependencies are complete; downstream units import only proved modules, never draft scaffolds (Appendix F.1, pp.26-27)
6. each proving run works in its own workspace so an unfinished unit is not visible to the project as complete (Appendix F.1, p.26)

Verus form. Inference: units map to Rust modules or functions, the graph to the call and use graph, and the import of proved modules only to letting an agent call only functions whose bodies already verify, as opposed to ones whose contract is merely stated. Inference: the lints in step 4 have direct textual counterparts between a requirement and a contract: <==> turned into ==>, < turned into <=.

evidence: ODENumLib, 23 units of which 20 closed (Appendix D, p.19). No ablation.

technique 7: a compiling statement scaffold fixed before proof search

what it is: the planner emits the root statement and one tagged declaration per planned lemma, all with placeholder bodies, and makes them read-only during proving.

how it is done (§2.1, p.3; Appendix F.2, p.27):

1. review the natural-language proof for gaps and translate it into a lemma-level graph; check it for dangling edges, self-loops, target reachability and references to source steps
2. collect candidate library lemmas from three search tools and check every name against the live environment before showing it to the model
3. emit the scaffold. “The statement scaffold deliberately leaves theorem bodies as := by sorry.” (Appendix F.2, p.27)
4. a compile-and-quality pass checks that the root declaration exists, rejects vacuous targets such as True, and checks every blueprint node has a tagged declaration
5. the scaffold is read-only during proof search; the prover implements it in Basic.lean and may introduce helper lemmas (§2.1, p.3; the proof DAG may grow with them, Appendix F.2, p.27)

Verus form. Inference: write each planned proof fn and each executable function with full requires and ensures and a body that is only assume(false) or admit(), check the crate verifies in that state (so the lemmas, taken as given, do imply the root), then replace bodies one at a time with the signatures locked. Inference: step 4’s vacuity check becomes rejecting ensures true and a requires that no input satisfies.

evidence and limits: not ablated. In ODENumLib the final main theorem differs substantively from the retained scaffold in nine of the 19 units that kept one (Appendix D, p.19; this study counts nine ∆ rows in Table 9, p.20), Inference: so in that project the final statements did not stay at the scaffold; the paper does not say whether the read-only rule applied then, and it says some changes repair an inadequate scaffold.

technique 8: advice that cannot become proof

what it is: every source of help other than the prover (human, supervisor model, mined skills) reaches the prover through a channel that cannot change statements, code or state.

how it is done (Appendix F.4, p.28):

1. supervisor and human advice enter as comments only. “ORCHESTRATOR advice is inserted only as non-executable comments.” (Appendix F.4, p.28)
2. the supervising model has no file, shell, web or Lean-write access; a restricted sidecar does file changes
3. the sidecar watches for stagnation: an unchanged positive sorry count, repeated blockers, iterations with no prover edits; these trigger review or extra critic agents
4. skills mined from finished runs are admitted by code. “Every lemma named by a candidate skill is checked against the live Lean environment, and only fully verified, actionable skills pass the strict retrieval gate.” (Appendix F.4, p.28)
5. one gateway process is the only writer of stage state, and stage advancement is derived from persisted artifacts and exit status (Appendix F.1, p.26)

Verus form. Inference: carries over unchanged, since nothing in it depends on the prover; step 4 becomes checking that every lemma or broadcast group a stored hint names exists in the current vstd and project.

evidence: none. “We do not attribute an independent empirical effect to CURATOR in this paper.” (Appendix F.4, p.28); the same is said of supervision.

where the paper disagrees with itself

• the abstract and §3.4 present ODENumLib as evidence that Fyan sustains a document-level project, and the paper’s central component is the audit. Appendix D says: “It was built before the semantic audit was added to FYAN, so its statements were accepted on compilation and the completion gate alone.” (Appendix D, p.19). So no experiment in the paper runs the audit, the bridge and the proving loop together.
• §3.4 and Table 5 say 20 units; Appendix D says the project has 23, three still open (one never built, one with two sorry, one with six; Table 9, p.20). Only 17 of the 20 replay under the pinned Lean and Mathlib.
• Table 5 counts a unit as formalized when it has no sorry and no new axiom, yet Table 9 lists runge_kutta_4 as passing with the local defect assumed as a hypothesis, and convergence/dahlquist as proving one direction of the stated result (Appendix D, p.20).
• Inference: the headline recall gain (0.777 against 0.636) uses labels relabelled by the authors; under the benchmark’s own labels the audit is the less accurate method.
• the arithmetic was rechecked for this study: Table 2 percentages, every rate in Tables 3 and 7, 98/150, 124/143, 124/150, 216/343, 859 − 10 − 14 = 835, the Table 9 line counts summing to 9,355 over the 20 closed units, and the Fisher value 0.0056 all agree with their fractions.

already done here, so not for VL to rebuild

• the polarity rule with omissions as ⊤ and ⊥ and the table of quantifier-domain adapters (Appendix E)
• the record schema and the judge prompt, printed in full (Appendix G.2, pp.31-32)
• the six-condition completion gate
• the finding that BEq+ equivalence to a reference undercounts: 91 of the 143 FormalTCS references declare their own structure, inductive or class, and all 5 statements of the control harness that BEq+ certified are among the other 52 (Appendix C.1, p.17). Inference: grading an agent’s Verus spec by provable equivalence to a reference spec will fail the same way whenever the reference declares its own spec fn or type.

how much threat to a product of agent-written verified Rust

Inference, all of it. Low as a competitor: Fyan targets mathematics in Lean, has no notion of executable code, and its one large case study did not use its audit. High as a statement of the product’s weakest point: the Appendix D inventory is a measured instance of statements changing during proving (nine of 19 scaffolds changed substantively, some repairing an inadequate scaffold and others weakening the result by the paper’s account; 7 of 343 ProofNet# signatures changed, counted as failures), which is the failure a verified-Rust product must exclude to mean anything. The audit design is reusable as is, and 46 of 206 misses with a small model shows it is a filter, not a guarantee.

techniques for the catalog

• slot-paired statement audit — cut informal source and formal contract into binder, hypothesis, goal and definition slots by code, have a model relate paired groups, and let code score every unpaired slot as an omission
• source-first extraction — build and independently review the quoted formula tree of the requirement before the model sees any formal text
• meaning checklist — ask six fixed questions of the original text: hypotheses present, no hidden extra conditions, conclusion strength, notions realized by their bodies, domain and type edge cases, non-vacuity
• polarity rule — conclusions may be strengthened and assumptions weakened, never the reverse, with the sign flipping under negation and on the left of an implication
• omission as ⊤ or ⊥ — model a deleted conjunct as true and a deleted disjunct as false so that omissions obey the polarity rule instead of a special case
• quantifier-domain adapter — accept a changed variable domain only with a map in the direction fixed by quantifier kind and polarity
• minimum-grade verdict — grade each row 0 to 3 and take the minimum, computed by code, so one unresolved item fails the statement
• closed conversion list — allow “trivially equivalent” only when the row names a conversion from a fixed list
• no re-vote, fail closed — repair a malformed record’s form but never resample a valid unfavorable one, and treat no valid record as rejection
• bridge obligation — admit a non-identical statement only with a machine-checked proof that it implies an audited source-facing statement
• frozen signature — bind the accepted statement to its source and definitions so any later edit voids the certification
• completion gate without a model — decide “done” by placeholder count, build, signature currency, bridges, certification and transitive axiom audit
• graph checked by code — let a model propose units and dependencies, then verify coverage and acyclicity and recompute the order deterministically
• statement scaffold — fix all planned lemma statements with placeholder bodies, reject vacuous targets, and lock them before proof search
• comment-only advice — route human, supervisor and mined-skill guidance through channels that cannot edit statements, proofs or state

Last edited: 2026-10-13