AutoGraphForge: Towards Automated Graph Theory Discovery
cs.AI · cs.LO · math.CO
Quick verdict
Honest systems paper: 6,522 conjectures survive a 348K-graph refutation loop; Lean proving stage only sanity-checked; strong pipeline, modest verified yield.
Summary
AutoGraphForge is a computational pipeline that automates graph-theoretic discovery through four coupled stages: conjecture generation, refutation, formalization, and proving. A Graffiti3-style generator proposes linear inequalities over a small snapshot table that grows from 337 to 2,860 graphs purely by counterexamples; a novelty filter built from 559 known relations, closed under transitive composition and linear substitution, uses linear programming to discard candidates already implied by the literature. Survivors are attacked by a 348,207-graph refutation dataset (House of Graphs export, the complete census of connected graphs up to nine vertices, and 46,156 extremal-family graphs), parametric families, random models, and six active search algorithms. Five partitions on 256-core cluster nodes consumed 1.22 CPU-years, yielding 8,281 raw survivors that merge to 6,522 (2,677 class-conditioned inequalities, 3,845 Sophie conditions); the author hand-proved two relations between the annihilation number and the edge-cover number. The Lean 4 stage integrates DeepSeek-Prover-V2-671B and OProver-32B behind kernel verification but has confirmed only trivial inequalities, so the loop remains open. Main limitations: the proving stage is unevaluated, active search contributed little at untuned default settings, and no truth-rate estimate exists for the 6,522 survivors.
Review complete
Assessment at a glance
4
risk flags identified
● high 0
● medium 2
● low 2
5 strengths · 5 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- AutoGraphForge integrates conjecture generation, LP-based novelty filtering, dataset-plus-active-search refutation, and Lean 4 formalization/proving in one pipeline, with the first three stages running end-to-end at scale.
- The generate–refute loop over five HPC partitions (1.22 CPU-years) produced 8,281 raw surviving conjectures, merged to 6,522 after cross-partition refutations (1,413) and duplicate removal (346).
- Two nontrivial relations between the annihilation number and the edge-cover number, for bipartite and for regular graphs, were proved by hand.
- The deterministic Lean 4 export plus kernel-checked neural provers (DeepSeek-Prover-V2-671B, OProver-32B) is integrated end-to-end but has so far verified only deliberately trivial inequalities; the loop is explicitly not closed.
- Static/parametric datasets dominate counterexample yield, while six active-search algorithms at default hyperparameters contributed only 1–22 counterexamples per round.
Strengths
Unusually honest scope statement
The abstract and §1 state explicitly that the loop is not closed: the first three stages run end-to-end at scale while the proving stage is implemented and sanity-checked only, having kernel-verified just two deliberately trivial inequalities (δ≤Δ, ω≤n). No overclaiming of the Lean results.
Invariant soundness discipline (§3.1)
GraphCalc values are cross-checked against a networkx registry via a per-run unit test, and against independently computed House of Graphs values on 2,500 graphs with zero mismatches on all shared invariants (χ, α, ω, γ, ν, Δ, δ, κ, λ, diam, tri, booleans) — directly addressing failure modes 1 and 5 the paper itself enumerates.
Novelty filter validated by rediscovery (§3.3, §4.1)
Transparent run accounting (Table 1, §4.1)
Tiered refutation strategy is empirically justified
Weaknesses
Proving stage essentially unevaluated
No truth-rate estimate for the survivor set
Active search contribution is marginal and untuned
Refutation census reaches only n≤9
Thin mathematical yield relative to compute
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
This ITAT 2026 workshop paper (arXiv:2609.03478) reports AutoGraphForge, an automated conjecture–refutation–formalization–proving loop for graph theory. The author is explicit that the first three stages run end-to-end at scale while the proving stage is implemented and sanity-checked only. Central claims: (i) 6,522 conjectures survive a 348,207-graph refutation dataset, a 559-relation novelty filter, and active counterexample search across five HPC partitions (8,281 raw survivors reduced by 1,413 cross-partition refutations and 346 duplicates); (ii) two relations between the annihilation number and the edge-cover number (bipartite and regular graphs) are proved by hand; (iii) a deterministic Lean 4 export plus kernel-checked DeepSeek-Prover-V2-671B and OProver-32B works, having verified only trivial inequalities (δ≤Δ, ω≤n).
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 5 strengths & 5 weaknesses, analyzed in detail
- 4 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What is AutoGraphForge?
It is a computational pipeline for automated discovery in graph theory. It generates conjectured inequalities between graph invariants, filters out statements already implied by 559 known results via linear programming, tries to refute survivors against a dataset of about 348,000 graphs plus active search algorithms, and translates what remains into Lean 4 statements for automated proving.
Did AutoGraphForge prove any new theorems?
Partly. The author hand-proved two relations between the annihilation number and the edge-cover number (for bipartite and regular graphs). The neural proving stage has so far kernel-verified only deliberately trivial inequalities (such as minimum degree ≤ maximum degree); the full proving evaluation was still running when the paper was written, and the authors explicitly state the loop is not yet closed.
How many conjectures did it produce and are they true?
Five HPC partitions (1.22 CPU-years total) yielded 8,281 raw survivors, merged to 6,522: 2,677 class-conditioned inequalities and 3,845 Sophie sufficient conditions. They are 'survivors' — no counterexample was found and they were not flagged as known — but the paper reports no estimate of how many are actually true or genuinely new.
Is the code and data available?
Yes. The paper states that all code, documentation, data, logs, and databases are available and under development at github.com/JanPastorek/AutoGraphForge, and the appendices specify the deterministic partition assignment and the search backends' hyperparameters.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- The provided text is a sampled excerpt: §3.5 (formalization details), §4.2 (containing the hand-proved theorems), and the conclusion fall in marked '[...sampling gap...]' regions, so the formal statements of the two proved theorems could not be checked.
- The reference list is cut mid-entry at reference [36] in the excerpt; later references are known only from in-text citations.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.