{"id":"bb7bdf52-6c07-4de2-ad8d-a06789f6e977","arxiv_id":"2607.13292","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Autoformalization should target complete theories—axioms, definitions, lemmas, proofs—as unified formal libraries, not isolated statements.","lead":"This position paper argues that autoformalization should translate whole theories—axioms, definitions, lemmas, proofs—into one formal library, not isolated statements. It lays out the challenges and three research paths for making machine-verified knowledge bases a practical goal.","discovery_kind":"review","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Central claim's urgency rests on unshown scalability of automated blueprint generation; the paper's own §4.2a concedes current decomposition methods handle only high-school-level shallow graphs, and §3.3 admits human blueprints remain expert-intensive. Without evidence this gap closes, 'necessary an","rationale":"The reader's weakest assumption precisely identifies the same load-bearing gap: the cost-reduction argument assumes LLM-based hierarchical decomposition and abstraction learning can scale from single statements to entire textbooks, generating blueprints with little expert effort. My analysis of the full text confirms this is the weakest point. The paper is a position paper, not a demonstration; it contains no implementation, no benchmark, and no machine-checked evidence for the central feasibility claim. The strongest sections, such as §4.1 on equivalence checking, are substantive and honest about the subjectivity of equivalence, and the survey of DSLs in §4.3 is useful. However, the conclusion that theory-level autoformalization is 'necessary and imminent' goes beyond what the evidence supports, because the only successful large-scale examples depend on human blueprints and the proposed automation of blueprint generation is admitted to be insufficient in current systems. This is not a fatal flaw—the direction may still be right—but it justifies a conditional verdict rather than full acceptance. The reader's CONDITIONAL verdict stands, so I recommend no change.","tokens_in":20132,"tokens_out":3616,"duration_ms":70081,"concrete_test":"Controlled study: formalize a textbook theory not yet in Mathlib (e.g., Chapter 2 of Rudin's Principles of Mathematical Analysis, roughly 40 definitions/lemmas) in Lean under three conditions: (A) the paper's proposed pipeline—a general-purpose LLM generates the blueprint dependency graph directly from textbook prose, with no human blueprint, then autoformalizes in topological order; (B) the Math Inc. human-blueprint pipeline—human expert writes the blueprint, LLM fills in lemmas; (C) statement-level autoformalization with incremental human library fixes. Measure expert time (hours), fraction of definitions/lemmas successfully formalized, and whether the resulting library is coherent and reusable (e.g., can state and prove a target theorem). If condition A requires expert effort within roughly 2x of condition B or fails to produce a usable library, the central cost-reduction argument fai","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that autoformalization must shift from isolated statements to theory-level formal knowledge bases. That claim is load-bearing on the premise that automated theory-level formalization can remove the human-blueprint bottleneck, making large-scale formalization dramatically cheaper. The paper itself supplies evidence against this premise. In §3.3 (counterargument to View 3), the authors concede that human blueprints 'still require substantial time and effort from human experts.' In §4.2a, they state that current decomposition methods (DNA, DRIFT, Aria) 'handle only high school mathematics with shallow dependency graphs' and 'remain insufficient for theory-level blueprint generation.' The only large-scale successes cited (Math Inc. 2025a,b, 2026) are semi-theory-level projects with human-written blueprints. The leap from 'statement-level autoformalization + human blueprint works' to 'LLM-generated blueprints for entire textbooks will scale with little expert effort' is not supported by any experiment or mechanism. If blueprint generation stays expert-intensive, theory-level autoformalization is not a qualitatively new capability but a relabeling of semi-automated formalization, and the field's shift is not 'necessary and imminent' but one research direction among several. This is a correctness risk in the argument itself, not merely a disagreement with current consensus.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This position paper argues that autoformalization research should move from translating isolated informal statements into formal ones to constructing complete, interdependent formal theory libraries. It defines theory-level autoformalization, motivates the shift through real-world formalization projects, the dependence of statement-level tasks on existing libraries, and the role of new abstractions in mathematical discovery. It then considers and rebuts three alternative views, identifies four open challenges (equivalence checking, hierarchical decomposition and abstraction learning, low-resource DSLs, and multimodal inputs), and makes three proposals (theory-level benchmarks, general-purpose LLMs, and a common intermediate representation). The paper is a synthesis and position statement rather than an experimental study.","tokens_in":20459,"tokens_out":5892,"duration_ms":69947,"significance":"If accepted, the thesis would redirect evaluation and system design from statement-level benchmarks to library-scale formalization, with implications for neural theorem-prover training data, verification speed, and the formulation of new mathematical abstractions. The paper's strengths are its clear articulation of an important problem, the critical analysis of equivalence checking in §4.1, the useful taxonomy of low-resource DSLs in §4.3, and the survey repository. However, the force of the central claim depends on the unexamined assumption that automated blueprint generation can scale; the paper's own survey indicates this is not yet established. With revision to temper the urgency claim and to sharpen the research agenda, the paper could serve as a useful agenda-setting contribution.","major_comments":[{"comment":"The central thesis ('necessary and imminent', §2.2) rests on the premise that automated theory-level formalization can replace human blueprints. The paper itself supplies evidence against this premise: §3.3 concedes that human blueprints 'still require substantial time and effort from human experts,' and §4.2a states that current decomposition methods (DNA, DRIFT, Aria) 'handle only high school mathematics with shallow dependency graphs' and 'remain insufficient for theory-level blueprint generation.' No experiment or mechanism is offered for closing this gap. If blueprint generation remains expert-intensive, the contribution is a repackaging of semi-automated formalization rather than a new capability. I recommend either softening the 'necessary and imminent' conclusion or adding a concrete test—e.g., the expert-effort measurement in §5.1—and making the scalability of blueprint generati","section":"§2.2c, §3.3, §4.2a"},{"comment":"Proposal 1 asks for benchmarks with 'sound equivalence checking' (criterion ii), but §4.1 convincingly shows that no checker combining soundness with practical coverage exists and that formal-formal equivalence is inherently subjective (§4.1c). As stated, the benchmark criterion is unsatisfiable. It should be restated as equivalence relative to a restricted admissible fragment—as BEq+ does in §4.1b—with precision and recall against expert judgments reported, not blanket soundness. This is not a cosmetic change: it determines what can be measured and therefore what the benchmark actually rewards.","section":"§4.1c, §5.1"},{"comment":"The argument that statement autoformalization implies theory-level autoformalization relies on a conflation. For domains outside existing libraries, the main work is constructing the missing formal context, but that can be done incrementally, on demand for the target statements. The paper defines theory-level as formalizing 'the entire theoretical context ... as a coherent formal library' and speaks of 'holistic formal knowledge bases' (Abstract, §6). The step from 'dependencies are needed' to 'whole theories must be formalized as unified artifacts' is not automatic and is not supported by the survey. The paper should either define theory-level to include incremental dependency construction or justify the added holism requirement.","section":"§2.2b"},{"comment":"The claim that formalizing entire theories will enable discovery of new abstractions ('refactoring this codebase allows us to identify common structures ... eventually use these new abstractions to prove new results') is speculative. Historical examples show humans inventing abstractions; they do not show that a formal corpus is either necessary or sufficient for such invention. Library learning in program synthesis (Ellis et al., 2021) and theorem proving (Zhou et al., 2022) operates on much smaller scales and does not generate new mathematical abstractions. This is acceptable as a long-term motivation, but it should be separated from the 'necessary' claim so that the argument's load-bearing assumptions are explicit.","section":"§2.2c"}],"minor_comments":[{"comment":"The claim that 'the best current method achieves 71.4% on statements in Layer 3' (Min et al., 2026) needs the task and metric specified: is this statement autoformalization accuracy, proof autoformalization, or something else? Which dataset? Without this, the number is hard to interpret.","section":"§2.2"},{"comment":"Figure 7 is central to Proposal 3 but not described in enough detail. A concrete example showing how a multimodal input (e.g., a timing diagram plus text) would be represented in the common IR would make the proposal more actionable.","section":"§4.3, Figure 7"},{"comment":"The distinction between declarative and imperative synthesis is helpful, but 'contains strictly more information' is intuitive rather than formal. Consider connecting this to the equivalence discussion in §4.1: a semantics-preserving translation is one for which the equivalence check passes under an appropriately restricted fragment.","section":"Appendix A"},{"comment":"There are several typos and formatting issues: 'Goedel' should be 'Gödel', 'V oronkov' has a stray space, and the Abstract's survey URL is line-broken. A careful proofreading pass is needed.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The paper is a position paper, so the absence of experiments is not itself a defect. The main risk is that the authors' own prior work (Min et al., 2026) and affiliated Math Inc. projects are used as evidence for scalability; I did not find this circular, but the independent evidence base is thin. The revision should make the 'necessary and imminent' language formally weaker and convert the blueprint-generation bottleneck into an explicit open research question with measurable milestones."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bottom line: this is a genuinely useful position paper, not because it proves anything new, but because it gives the field a label and a coherent way to talk about whole-theory formalization. The survey is broad and careful, and the discussion of equivalence checking in §4.1 is the best short treatment I've seen: the distinction between exact match, logical equivalence, definitional equivalence, and the subjectivity of formal-formal equivalence is concrete and correct. The example with n*1=n versus n+0=n is a nice way to show why any checker needs a threshold. That section alone is worth a cite.\n\nThe tower framing (axioms, definitions, tooling, target theorems) is helpful, and the proposals in §5 are reasonable. General-purpose models over fine-tuned specialists is a defensible position, and the common IR idea is at least worth arguing about.\n\nThe soft spot the reader flagged is real, and it lands. The central claim—that the field must shift, and that this shift is 'necessary and imminent'—depends on scaling automated blueprint generation from high-school-level statements to entire textbooks. The paper itself concedes, in §3.3 and §4.2a, that human blueprints require substantial expert effort and that current decomposition methods handle only shallow dependency graphs. There is no mechanism or experiment showing that gap closes. So the urgency claim is overstated, and the paper would be more honest if it framed theory-level formalization as one important direction among several, not 'the' inevitable path.\n\nHaving said that, the paper is aware of its own limitations and does not hide them. For a position paper, that is good behavior. The citations to the authors' own DNA and Goedel results are illustrative, not load-bearing, so I don't see a circularity problem. There is no critical flaw. It is not a new result, and anyone expecting a benchmark or a proof will be disappointed. But as an agenda-setting survey, it is solid.\n\nWho is this for? Researchers in autoformalization, neural theorem proving, and formal verification. It would make a good reading group paper, and I would cite the equivalence-checking discussion. It deserves serious peer review—send it to referees, with the expectation that the authors should temper the 'necessary and imminent' language and address the blueprint-scalability assumption more directly.","headline":"A well-organized position paper that usefully names the theory-level shift and nails the equivalence-checking problem, but overstates the urgency when the hard part—automated blueprint generation—is still unshown.","tokens_in":20931,"tokens_out":2554,"would_cite":true,"duration_ms":22222,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Autoformalization must stop translating isolated statements and start building complete, interconnected formal libraries of theories.","keywords":["autoformalization","theory-level","formal knowledge base","theorem proving","formal verification","abstraction learning","domain-specific languages","multimodal input"],"falsifier":"Run an end-to-end case study formalizing a previously unformalized graduate-level theory chapter with and without a human-written blueprint under identical expert time budgets. If removing the blueprint does not reduce total expert effort relative to traditional formalization, the theory-level scaling claim fails.","tokens_in":20056,"feed_emoji":"📚","tokens_out":4771,"duration_ms":49518,"temperature":0.7,"pith_summary":"This position paper argues that the field of autoformalization—translating natural-language mathematics and engineering text into machine-checkable form—has set its sights too low. Real formalization projects, from the verification of major theorems to compilers and hardware, succeed only after a whole web of axioms, definitions, lemmas, and notations is in place; current systems treat that context as given. The paper claims that the next step is theory-level autoformalization: automatically constructing entire formal theories, with all dependencies, as coherent libraries. It argues this is necessary for scaling verification, for synthesizing training data for theorem-proving AI, and ultimately for discovering new mathematical abstractions. It then identifies the missing pieces—sound equivalence checking, hierarchical decomposition, abstraction learning, low-resource domain languages, and multimodal input—and proposes benchmarks, general-purpose models, and a common intermediate representation as a way forward.","feed_headline":"Autoformalization must build whole theories, not single statements","feed_subtitle":"Statement-level success hides the real bottleneck: axioms, definitions, and lemmas must come first.","key_machinery":"The argument is carried by the 'Theory-Level Autoformalization Tower,' a four-layer model of how any formal theory is built: axiomatic primitives at the base, derived definitions above them, proof infrastructure (notations, lemmas, tactics) in the middle, and target theorems at the top. It makes visible why statement-level translation implicitly assumes all lower layers already exist. The paper's proposed forward machinery is a common intermediate representation that can express multiple domain-specific languages, be type-checked and verified, and embed target languages for verified translation—turning the problem of supporting many niche domain-specific languages from combinatorial into lin","core_discovery":"On the paper's own terms, the central discovery is a reframing: autoformalization is not a statement-translation task but a theory-construction task. The authors define Theory-Level Autoformalization as formalizing the full theoretical context—axioms, definitions, notations, examples, lemmas, theorems, proofs, tactics, and their inter-dependencies—as a single coherent formal library. Their key evidence is structural: even a single theorem like the Pythagorean theorem requires lower layers of primitives, derived definitions, and proof tooling before it can even be stated. They argue that statement-level success so far has been an artifact of leaning on mature human-built libraries, and that g","pith_inferences":["If theory-level autoformalization reaches maturity, the binding constraint on formal proof shifts from proof search to abstraction design; systems that can propose new definitions and reorganize libraries may matter more than systems that prove given statements.","The paper's subjectivity argument about equivalence suggests that evaluation will need interactive or human-in-the-loop equivalence checking for hard cases, not only fully automated judges—a design choice the paper leaves open.","A concrete testable extension: build a benchmark where the same theory is formalized twice with deliberately different but equivalent definitions; a sound theory-level checker should still recognize the two libraries as equivalent. No current checker would pass this.","The common-intermediate-representation proposal implies a transfer test: success on formalizing one well-supported mathematical domain should transfer to formalizing a legal or security-policy text, since both reduce to building a coherent dependency graph of concepts."],"forward_implications":["Benchmarks and leaderboards would shift from accuracy on isolated statements to coherence and verifiability of whole libraries, with sound equivalence checking reported alongside precision and recall.","Theorem-proving AI would train on structured, dependency-linked corpora rather than flat statement-proof pairs, potentially improving generalization to new domains.","Verification of software, hardware, protocols, and access-control policies could be accelerated because the bottleneck—formalizing the surrounding specification context—would be automated rather than expert labor.","A common intermediate representation could make progress in mathematical autoformalization directly reusable for low-resource domain-specific languages, including declarative policy languages.","The eventual pay-off is a formalized knowledge base large enough to refactor, exposing common structure across domains and enabling proofs of results that cannot currently even be stated."],"fun_headline_variants":["Autoformalization's next step: entire theories, not just theorems","Move over single statements: Autoformalization goes theory-wide","Formalizing whole theories: the real autoformalization challenge","From isolated lemmas to unified formal knowledge bases","Autoformalization: build the theory, not just the theorem"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The cost-reduction argument assumes that language models can generate the hierarchical blueprint—the decomposition of a whole theory into lemmas and dependencies—with little expert effort, a capability demonstrated so far only for single statements or with human-authored blueprints.","fun_headline_variants_meta":{"raw":{"variants":["Autoformalization's next step: entire theories, not just theorems","Move over single statements: Autoformalization goes theory-wide","Formalizing whole theories: the real autoformalization challenge","From isolated lemmas to unified formal knowledge bases","Autoformalization: build the theory, not just the theorem"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000191,"raw_usage":{"total_tokens":1121,"prompt_tokens":627,"completion_tokens":494,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":371,"completion_tokens_details":{"reasoning_tokens":411}},"tokens_in":371,"tokens_out":494,"duration_ms":5169,"temperature":1.0,"reasoning_tokens":411,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T05:35:25.941281+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run an end-to-end case study formalizing a previously unformalized graduate-level theory chapter with and without a human-written blueprint under identical expert time budgets. If removing the blueprint does not reduce total expert effort relative to traditional formalization, the theory-level scaling claim fails.","supporting_citations":[],"review_version":1}