{"id":"252842ca-deff-49de-8d5f-2133d4faee7c","arxiv_id":"2602.15511","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"Proof-structure enumeration, combined with lemma synthesis by DAG compression and combinatory proof patterns, generates proofs for 734 of 1,374 Metamath-derived propositional theorems and improves prover success rates.","lead":"This paper presents methods for automatically generating theorems and their proofs from a small set of axioms, without being given a target statement. On a benchmark extracted from the Metamath database, the methods prove 734 of 1,374 theorems, and the synthesized lemmas substantially boost the success of first-order theorem provers.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"POI results are selected from a larger test set and tuned on the benchmark; without held-out evaluation the headline improvements may not transfer.","rationale":"The reader's weakest assumption is the lemma-value hypothesis in Sect. 6. That is a real concern, and the reader correctly notes it is validated only on the same benchmark corpus. My stress-test identifies a broader and more load-bearing issue: the paper's evaluation protocol allows configuration selection on the target benchmark, so even the direct POI improvements are best-case selections rather than fixed-pipeline results. The disclosed statements in Sects. 6 and 7 about choosing runs from a larger test set, plus the benchmark-informed combinator inventory in App. G, create a circularity between method development and evaluation. This does not make the generated proofs unsound—the artifacts and Appendix H show specific DAG grammar proofs that can be expanded to axiom-only proofs—but it does mean the central claim that the method is a working way to invent useful lemmas is not yet supported beyond the specific POI setting. A held-out or cross-benchmark evaluation would settle this. I found no internal mathematical error in the proof construction, save-value calculation, or the combinator-to-axiom conversions; the paper is careful and the appendices provide substantial evidence. Therefore my concern reinforces rather than overturns the reader's CONDITIONAL verdict, and I recommend no verdict change.","tokens_in":65300,"tokens_out":6099,"duration_ms":64243,"concrete_test":"Hold out a random 20% of POI before any configuration search. Use the remaining 80% to select all parameters (level characterization, Trim, GMax, combinator set, N_Lem, and the subset of runs) exactly as the paper describes, including the run-selection rule. Then measure on the held-out 20%: (i) the number of POI theorems proved by SGCD with the selected configuration, and (ii) the Vampire/leanCoP success when the synthesized lemmas are supplied. Repeat for at least three random splits. If the held-out recall and prover boost drop substantially relative to Tables 8 and 9, the reported gains are partly an artifact of benchmark-specific tuning; if they remain comparable, the central claim transfers.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central inference—that proof-structure enumeration plus DAG-compression lemma synthesis and combinator patterns is a working method for inventing useful lemmas—rests on the numbers in Tables 8 and 9. Those numbers, however, are not produced by a single fixed pipeline. Section 6 states that \"runs were chosen from a larger test set such that taken together they provide proofs for a large number of POI theorems not in POI-base\" (the same is said in Sect. 7), and App. G derives the combinator inventory by analyzing the very same set.mm fragment from which POI was built. The lemma-prefix lengths N_Lem, the level characterizations, and the run parameters were selected after seeing POI results. Hence 734/1374 and the Vampire/leanCoP boosts are best-case over configurations, not expected performance of the algorithm. This does not invalidate the existence of the generated proofs (the artifacts contain them), but it undermines the broader claim that the method transfers to other axiom systems or corpora. The Appendix D control (save-value vs. MGT-size ordering) is a useful step, but it is still on the same benchmark with the same run-selection freedom. The paper's protocol does not distinguish a general method from an overfit to POI; that is the load-bearing weakness.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"Starting from condensed detachment over the three classical propositional-logic axioms of set.mm, the paper defines inductive level characterizations of proof terms (tree size, height, PSP) and uses a configurable prover SGCD to enumerate proof-term levels bottom-up. A benchmark POI of 1,374 theorem formulas is extracted from a fragment of set.mm. A baseline enumeration proves 554 theorems. The paper then adds two mechanisms: lemma synthesis by minimal-DAG compression with save-value ordering, and combinator-based proof patterns/schemas. On selected SGCD runs the union of these methods proves 734 POI theorems (12 with rating 1), and the synthesized lemmas substantially raise the number solved by Vampire and leanCoP. The paper supplies extensive run tables, proof listings, and an appendix with per-theorem results.","tokens_in":65656,"tokens_out":6161,"duration_ms":67271,"significance":"The contribution is potentially significant: it gives an explicit proof-structure-based approach to goal-free theorem and lemma generation, with a concrete benchmark, reproducible artifacts, and external first-order prover checks. The described control experiment in Appendix D (save-value vs MGT-size ordering) is a useful step toward isolating the mechanism. If the method transfers beyond the calibration corpus, the paper would be a solid advance in automated lemma synthesis. The main reservation is that the headline numbers are produced by configuration selection on the same benchmark used for evaluation; this limits, for now, the strength of the general claim.","major_comments":[{"comment":"The paper's central empirical claim—that the method generates 734/1374 POI theorems and improves Vampire/leanCoP from 74% to 94% and from 7% to 44%—is an upper envelope over configurations. Section 6 states that 'runs were chosen from a larger test set such that taken together they provide proofs for a large number of POI theorems not in POI-base,' and Section 7 repeats: 'Again, runs were chosen from a larger test set...'. The same selection is also used for the lemma-enhanced prover experiments in Table 9. No size of the larger test set or selection protocol is given, and no held-out subset or separate axiom system is used. As a result, the 734 count and the prover boosts are best-case results, not expected performance of a fixed algorithm. I ask for either (a) an out-of-sample evaluation with a fixed default configuration and no selection after seeing results, or (b) an explicit, quant","section":"§6, Table 8; §7, Tables 10–11"},{"comment":"The combinator inventory is extracted from λ-to-SKI translations of the same set.mm fragment used to form POI, and the candidate combinator sets are selected by frequency in those same proofs. This creates a tuning loop: the proof schemas are chosen because they occur in the corpus, and their success is then measured on theorems from the same corpus. The claim that combinator proof patterns are generally useful therefore lacks an independent test. A concrete fix is to test with combinators chosen from a disjoint corpus or from a principled basis (e.g., all combinators up to a bounded arity/size), and to report sensitivity of Tables 10 and 11 to the combinator inventory.","section":"§7, App. G"},{"comment":"The value hypothesis behind the whole lemma-synthesis workflow—that save-value in a proof DAG measures mathematical usefulness—is an unproven heuristic. Appendix D is a valuable internal control, but it is still on the same POI benchmark and inherits the run-selection issue of Table 8; it shows that save-value beats MGT-size ordering within this corpus, not that the correlation holds more generally. To make the synthesis workflow robust, add a comparison against simple baselines (e.g., random lemmas or lemmas sorted by formula size) with fixed run selection, or an evaluation on a different axiom system. Otherwise the improved prover results may not transfer.","section":"§6, 'Computing the Lemmas'"}],"minor_comments":[{"comment":"The sentence 'Its seems useful for a systematic understanding...' contains a typo: 'Its' should be 'It'.","section":"§8"},{"comment":"The Schemas column uses notation such as 'dB,B4,C4,S' and 'dC4(C4(C4(C4C)))/1' that is not explained in the table or its caption; the 'd' prefix for direct proof schemas is defined only in the text. Please make the table self-contained or add a pointer.","section":"Table 11"},{"comment":"The phrase 'Drastic boost-ups' is informal; consider 'large increases' or substituting a quantitative statement of the improvement.","section":"§6"},{"comment":"Figures 1 and E show nearly identical precision plots. One of them could be omitted or reduced to a single representative sequence to save space.","section":"Fig. 1 and App. E"}],"recommendation":"major_revision","confidential_remarks":"To the editor: I regard the manuscript as technically sound at the level of individual proofs and quite transparent, but the experimental protocol is the central weakness. The authors' own statements in Sections 6 and 7 concede run selection from a larger test set, and Appendix G shows that the combinator choices were harvested from the same set.mm fragment. This is not dishonest reporting, but the paper's title and conclusion overstate the status of the method. I would like to see an out-of-sample or fixed-pipeline evaluation before publication; the paper is close enough that I would not recommend rejection if the authors can add such an experiment or, failing that, substantially weaken the generality claims and add a quantified discussion of the selection bias."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is worth your time if you care about automated theorem proving or lemma generation. It introduces the POI benchmark (1,374 theorems extracted from set.mm in classical propositional logic), a clean conversion pipeline, and two genuinely new techniques: lemma synthesis by DAG-compression save-values, and combinatory proof schemas. The reported improvements are concrete: with synthesized lemmas, Vampire goes from 74% to 94% on POI and leanCoP from 7% to 44%. Proofs for 734 POI theorems, including 12 rated hardest by the external provers, are presented with full proof-term listings. That is real evidence, and the Appendix D control (save-value ordering beats MGT-size ordering, 143 vs 94 new proofs) is a good internal check. The citation pattern is fine; the earlier SGCD/PSP work is cited, and the relation to Schulz's and Kaliszyk/Urban's save-value work is acknowledged. The soft spots are mostly about generalization, not correctness. The paper openly states that the SGCD runs in Tables 8 and 10 were chosen from a larger test set to maximize POI coverage, and the combinator inventory in Appendix G was derived by analyzing the same set.mm fragment from which POI was built. So the headline 734/1374 and the prover boosts are best-case over configurations, not expected performance of a fixed pipeline. The central hypothesis that proof-DAG compression correlates with lemma usefulness is validated only on this one benchmark, with no out-of-sample test. The announced code was not yet available at review time, so reproducibility currently rests on the detailed tables and proof listings. None of this invalidates the existence of the generated proofs or the value of the benchmark; it just means the paper should be read as proposing and demonstrating a method, not as establishing a general law. Who should read it: automated reasoning researchers working on lemma synthesis, proof structure enumeration, connection methods, or Metamath-based corpora. It deserves serious peer review. For the revision, I would ask for either a held-out evaluation or a much clearer separation between existence results and transferable performance claims, plus release of the code. Send it to review; a good referee will push on the run-selection issue without dismissing the work.","headline":"A solid, honest subfield contribution that introduces a useful benchmark and two working lemma-generation ideas; the headline numbers are real but best-case, chosen from a larger run set, so treat the transfer claims with caution.","tokens_in":684,"tokens_out":756,"would_cite":true,"duration_ms":30501,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B35","68T15"],"pacs":[],"model":"deepseek-v4-flash","headline":"By enumerating proof structures and mining compressed proof DAGs, a machine can generate useful theorems from axioms alone — shown on 1,374 benchmark theorems, with 734 proofs found and one prover's success rate rising from 74% to 94%.","keywords":["theorem generation","lemma synthesis","proof terms","condensed detachment","DAG compression","combinatory logic","first-order theorem proving","proof structure enumeration"],"falsifier":"Run the same lemma-synthesis pipeline on a fresh, equally large formal development — for example, a different axiom system or a separate branch of a proof library that was not used to calibrate the method — and check whether the lemmas it synthesizes still raise prover success rates. Concretely: compute the save-value ranking on a held-out set of proofs, take the top-k lemmas, and compare the precision of that ranking against rankings by formula size or by random selection; if the compressed-DAG lemmas do not outperform the baselines on the held-out set, the compression-value hypothesis is fal","tokens_in":65153,"feed_emoji":"🧩","tokens_out":8240,"duration_ms":82499,"temperature":0.7,"pith_summary":"The paper tries to show that a machine can generate useful mathematical theorems, together with proofs, from a fixed set of axioms and no target theorem. Its approach enumerates proof terms by increasing structural complexity, using condensed detachment (modus ponens with unification), and keeps only those whose most general theorem is defined. A large collection of such proofs is then compressed into a minimal DAG, and the subproofs that save the most space are promoted to candidate lemmas; feeding those lemmas back as additional axioms substantially boosts existing first-order provers. On a benchmark of 1,374 theorems extracted from a well-known formal library, the combined method generates proofs for 734 theorems, including 12 rated hardest by the provers it compared against, and raises the best prover's success rate from 74% to 94% and another's from 7% to 44%. A careful reader should care because this is a concrete, largely parameter-free demonstration that useful lemmas can be discovered from proof structure alone, without human-chosen premises or goal-driven search.","feed_headline":"Proof-shape enumeration proves 734 theorems from axioms alone","feed_subtitle":"Mining compressed proof DAGs for reusable lemmas lifts a top prover's benchmark success from 74% to 94%.","key_machinery":"The central object is the proof term, a tree built by condensed detachment — essentially modus ponens with unification — whose 'most general theorem' (MGT) is the most general formula the proof proves, unique up to variable renaming. The paper partitions all proof terms into inductive level characterizations (by tree size, height, or compacted DAG size) that allow bottom-up, cached enumeration with restrictions such as subsumption. For lemma synthesis it compresses a large set of generated proof terms into its minimal DAG grammar and computes the 'save-value' of each production — the amount of grammar size that production saves across the whole set; productions with high save-value are promo","core_discovery":"The central claim is that theorems can be invented from axioms alone by enumerating proof terms in order of increasing structural complexity — using condensed detachment — and then treating the most 'compressing' subproofs of a large generated proof set as candidate lemmas. The paper demonstrates this on a benchmark of 1,374 propositional-logic theorems drawn from a well-known formal library, generating full proofs for 734 of them, including twelve that three mature first-order provers could not solve within an hour. Adding the synthesized lemmas back as axioms raised the strongest prover's success rate on the benchmark from 74% to 94% and a top-down prover's from 7% to 44%. The paper furthe","pith_inferences":["Because the save-value criterion is entirely structural, it may serve as a general proxy for 'mathematical centrality' in any proof corpus, not just this propositional benchmark; testing it on a different large library or on interactive proof assistants would show whether the correlation transfers.","The pipeline could be used as a data-augmentation source for learning-based premise selection: generate a large pool of candidate lemmas from axioms alone, then let a learned model filter them by predicted usefulness, rather than relying on human-curated lemma sets.","If the same enumeration scales to predicate logic, it would enable machines to propose lemmas in real mathematical domains without human-selected premises, effectively automating part of the invention step in formal mathematics; the paper notes the obvious next target is predicate logic.","The compression-value criterion resembles a minimum-description-length principle for proof libraries; one could test whether lemmas that maximize DAG compression coincide with lemmas humans choose to state and reuse across a broader mathematical corpus."],"forward_implications":["Synthesized lemmas can be appended as axioms to existing first-order provers, raising their success rates on the benchmark from 74% to 94% for the strongest prover and from 7% to 44% for a top-down prover.","The method generates full proofs for 734 of the 1,374 benchmark theorems, including 12 that mature provers could not solve within an hour, demonstrating that proof-structure enumeration can discover hard theorems.","The generated proofs are often far more compact in DAG size than the original human-written proofs, suggesting the enumeration can surface structurally simpler derivations from the same axioms.","The level-based enumeration gives a uniform, configurable framework in which different complexity measures and heuristic restrictions can be plugged in, and which links theorem generation to formulas-as-types and to grammar-based compression."],"fun_headline_variants":["Proof-term levels generate 734 theorems from axioms","Compressed proof DAGs mine lemmas, lift provers to 94%","Axioms alone: 734 theorems proven via proof structures","Enumerating proof shapes invents 734 theorems"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The method rests on the hypothesis that a formula is a genuinely useful lemma exactly when it appears as a shared subproof that significantly compresses a large set of generated proofs; this correlation is inferred from experiments on the same benchmark rather than independently proved or tested on out-of-sample axiom systems.","fun_headline_variants_meta":{"raw":{"variants":["Proof-term levels generate 734 theorems from axioms","Compressed proof DAGs mine lemmas, lift provers to 94%","Axioms alone: 734 theorems proven via proof structures","Enumerating proof shapes invents 734 theorems"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000583,"raw_usage":{"total_tokens":2527,"prompt_tokens":640,"completion_tokens":1887,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":384,"completion_tokens_details":{"reasoning_tokens":1816}},"tokens_in":384,"tokens_out":1887,"duration_ms":16837,"temperature":1.0,"reasoning_tokens":1816,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T22:47:23.426223+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the same lemma-synthesis pipeline on a fresh, equally large formal development — for example, a different axiom system or a separate branch of a proof library that was not used to calibrate the method — and check whether the lemmas it synthesizes still raise prover success rates. Concretely: compute the save-value ranking on a held-out set of proofs, take the top-k lemmas, and compare the precision of that ranking against rankings by formula size or by random selection; if the compressed-DAG lemmas do not outperform the baselines on the held-out set, the compression-value hypothesis is fal","supporting_citations":[],"review_version":1}