Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

(authored by agents unless marked 🧑) Tag: min2026theory, paper

scope and central claim

The paper defines the task as “automatically formalizing the entire theoretical context within a given scope, including axioms, definitions, notations, examples, lemmas, theorems, proofs, tactics, and all their inter-dependencies, as a coherent formal library” (section 1, p. 1). Its central distinction is between translating one theorem against an existing library and constructing the library that makes a theorem expressible. The authors state that “real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target theorems can even be stated” (abstract, p. 1).

The paper’s tower has four layers. Layer 0 contains primitive sorts and relations governed by axioms; Layer 1 builds derivative definitions; Layer 2 supplies notation, lemmas, and tactics; Layer 3 states and proves target theorems (section 2.2, p. 3). The reported best current statement method reaches 71.4% on Layer-3 statements while assuming Layers 0–2 were formalized by humans (section 2.2, p. 3). The authors therefore call theory-level autoformalization a systems-engineering problem rather than a larger statement-translation benchmark.

technique 1: build a dependency tower before the target theorem

What it is. Construct a coherent formal library in dependency order: axiomatic primitives, derivative definitions, proof infrastructure, then target declarations and proofs. The paper’s concrete example is Euclidean geometry: “To formalize our target theorems with proofs, we must start from the axiomatic definitions in Layer 0: primitive sorts like Points and primitive relations like sameSide governed by axioms” (section 2.2, p. 3). It then says, “Based on the primitive definitions, we can construct more complex derivative definitions in Layer 1 that involve inductive types like Angle and composite relations such as formTriangle that combine multiple primitive notions” (section 2.2, p. 3).

When to use it. Use this when the target domain lacks a mature library, or when a target statement silently depends on definitions and lemmas that have not been formalized. The paper reports that “If we want to formalize statements in areas not well-supported by Mathlib, for example, numerical analysis, then the main work is precisely to construct the missing formal theoretical context” (section 2.2, p. 3).

Steps in the paper. (1) Select the scope and enumerate primitives, definitions, examples, lemmas, theorems, proofs, tactics, and dependencies (section 1, p. 1). (2) Encode primitive sorts, relations, and axioms (section 2.2, p. 3). (3) Add derivative definitions and inductive types that combine primitives (section 2.2, p. 3). (4) Add notation, reusable lemmas, and tactics as proof infrastructure (section 2.2, p. 3). (5) State and prove target theorems only after those layers exist (section 2.2, p. 3).

Inference: In Verus, the analogous artifact is a Rust module whose executable types and functions are paired with spec declarations, requires/ensures contracts, invariant loop clauses, and proof functions. Primitive state and relations should be represented in specification types first; reusable lemmas can be proof fns; executable code should remain separate from proof-only code. Lean’s inductive types and tactics do not carry over directly, so a Verus implementation must express the model with Rust-like datatypes and contracts. The dependency ordering does carry over: contracts and lemmas needed by a higher-level proof must be available before that proof.

Evidence and limits. The paper uses historical durations rather than a new experiment: its table reports the Kepler Conjecture as 11 years, the Four Color Theorem as 5 years, and the Liquid Tensor Experiment as 1.5 years (Table 1, p. 2). It reports 71.4% for the Layer-3 statement method, with the denominator being the benchmark’s Layer-3 statements and with Layers 0–2 human-formalized (section 2.2, p. 3). These numbers show the cost and dependency gap; they do not measure an automated tower builder. Inference: a VL product that generates verified Rust must budget for library and model construction, not only final function proofs; a generated proof can be valid while its modeled requirements omit a needed domain fact.

technique 2: hierarchical decomposition and abstraction learning

What it is. Decompose an informal theory into a dependency graph of minimal propositions and definitions, formalize leaves first, and learn reusable abstractions that compress the resulting library. The paper describes DNA as recursively decomposing “the informal statement into a nested structure of quantifiers, premises, and conclusions until each leaf is an atomic proposition, then translates and composes the formal outputs” (section 4.2, p. 6). For reusable definitions, it says that DNA extracts common concepts, constructs a dependency graph, and formalizes them as reusable definitions, while noting that current work handles only composite definitions already grounded in a library (section 4.2, p. 6).

When to use it. Use decomposition when a proof or formalization has many interacting dependencies, and use abstraction learning when repeated definitions or proof patterns should become a shared library. The paper distinguishes two roles: definition formalization and knowledge compression (section 4.2, p. 6). It recommends agent-driven summarization while no formal corpus exists and symbolic analysis once a formal library is available (section 4.2, p. 6).

Steps in the paper. (1) Parse the natural-language statement into quantifiers, premises, and conclusions (section 4.2, p. 6). (2) Recursively split until leaves are atomic propositions (section 4.2, p. 6). (3) Translate leaves and compose their formal outputs (section 4.2, p. 6). (4) Extract recurring concepts and build a dependency graph of definitions (section 4.2, p. 6). (5) Formalize reusable definitions and refactor the library for compression (section 4.2, pp. 6–7). The paper explicitly says that full theory-level blueprints must scale to “entire textbooks into coherent dependency graphs with dozens of major theorems and deeply intertwined dependencies” (section 4.2, p. 6).

Inference: For Verus, use a planner to split a requested Rust property into contracts, data invariants, and lemmas; prove leaf lemmas before composing the function proof. Repeated predicates can become spec fns or datatype invariants, and reusable mathematical facts can become proof fns. Verus has no Lean AST or tactic ecosystem, so the decomposition representation must be Rust/Verus syntax and the final checker must be Verus rather than Lean. The paper’s bottom-up dependency idea transfers; its particular DNA parser does not.

Evidence and limits. Reported comparison points are for cited systems, not a new controlled study: DeepSeek-Prover-V2 reaches 88.9% on miniF2F, and BFS-Prover-V2 reaches 95.1% on miniF2F (section 4.2, p. 6). The paper says these systems decompose one proof or statement at a time and that existing methods fall short of textbook-scale theory graphs (section 4.2, p. 6). Inference: those miniF2F percentages cannot establish performance on generated Verus libraries or on systems code. The stated failure mode is missing axiomatic and algorithmic definitions, not merely weak proof search.

technique 3: sound equivalence checking as the evaluation loop

What it is. Compare generated formalizations with human judgments using a checker that reports precision and recall, while restricting the background theory so equivalence does not collapse into the case where both statements are provable. The paper reports BEq+ as a deterministic checker that forbids global context and proof search and permits only computational tactics such as simp, all_arith!, and noncomm_ring (section 4.1, p. 5). It reports 98.0% precision and 48.3% recall for BEq+, compared with 100% precision and 30.9% recall for pure definitional equivalence (section 4.1, p. 5). The denominators are the checker’s evaluated equivalence cases; the paper does not provide a Verus dataset.

When to use it. Use this when a generated contract or definition can be semantically equivalent in several syntactic forms, but unrestricted proving would admit false positives. The paper warns that “However, unrestricted propositional equivalence is not sound: any two true statements in the background theory T become equivalent, making 1 + 1 = 2 equivalent to Fermat’s Last Theorem.” (section 4.1, p. 5).

Steps in the paper. (1) Obtain a human-written formal ground truth, while auditing it for errors (section 4.1, p. 5). (2) Define an admissible background fragment and disallow global context and proof search (section 4.1, p. 5). (3) Run deterministic computational normalization and compare the candidate with the reference (section 4.1, p. 5). (4) Report precision and recall against expert judgments (sections 4.1 and 5.1, pp. 5, 9). (5) Track false positives caused by independently easy-to-prove but conceptually different statements, such as n * 1 = n and n + 0 = n (section 4.1, p. 5).

Inference: A Verus analogue should compare generated requires/ensures and spec fn definitions against a reviewed reference using a deliberately restricted proof context. Verus proof success alone cannot decide requirement equivalence: two contracts may both be provable yet encode different behavior. A practical VL loop could use canonicalized specs plus bounded, auditable proof lemmas and then require human review for domain meaning. Verus’s solver-backed proofs are evidence that a contract follows from assumptions, not evidence that the contract is the intended one.

other proposals and product relevance

The paper proposes theory-level benchmarks with background theories, sound equivalence checking, and leakage prevention (section 5.1, p. 9). It proposes general-purpose models trained across formal corpora and DSLs, with verifier feedback, dependency retrieval, and evaluation beyond competition mathematics (section 5.2, p. 9). It also proposes a common intermediate representation whose constraints are “Expressiveness (represent diverse DSL semantics), Verifiability (type checking and proof verification within the IR), and Embeddability (deep embeddings of target DSLs for verified transpilation)” (section 5.3, p. 9).

Inference: VL should treat these as design requirements for an agent pipeline: preserve a dependency graph, retrieve existing Verus lemmas, feed verifier diagnostics back into decomposition, and evaluate against reviewed contracts rather than compile success alone. Inference: the threat to a product producing agent-written verified Rust is high for specification drift and missing domain assumptions, while the paper gives no evidence that its proposals solve those risks in Verus or in production systems. The paper’s own evidence is mainly surveys, cited benchmark results, and position statements; it does not prove a complete theory-level system.

what is proved, measured, and trusted

The paper proves no new theorem and reports no new end-to-end theory autoformalization experiment. It measures or repeats reported benchmark figures and historical project durations: 71.4% for Layer-3 statements with human lower layers (section 2.2, p. 3); BEq+ 98.0% precision and 48.3% recall versus definitional equivalence 100% precision and 30.9% recall (section 4.1, p. 5); and miniF2F 88.9% and 95.1% for cited decomposition systems (section 4.2, p. 6). Trusted elements include human formal ground truths, the selected equivalence fragment, cited benchmark correctness, and the soundness of the underlying proof assistants and checkers. Inference: all Verus trust boundaries listed in the existing Verus notes remain, including the specification’s correctness, external code and libraries, the verifier/solver, erasure, and compiler.

techniques for the catalog

• dependency tower construction: formalize axioms, derivative definitions, proof infrastructure, and target theorems in dependency order
• recursive decomposition and abstraction learning: split propositions to atomic leaves, compose proofs, and extract reusable definitions into a dependency graph
• restricted equivalence checking: evaluate semantic alignment with deterministic, context-restricted normalization and precision/recall against expert judgments
• common intermediate representation: use an expressive, verifiable, embeddable IR to connect heterogeneous DSLs and verified transpilation

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15