AutoGraphForge: Toward Automated Discovery in Graph Theory

Summary

AutoGraphForge is an ongoing project for a computational pipeline that automates graph-theoretic conjecturing, refutation, formalization, and proving. Its conjecture-generation loop is counterexample-guided: Graffiti3 proposes relations over a small evolving table of graphs and computed invariants, and the table grows only with counterexamples to its own conjectures. A novelty filter containing 559 classical and folklore relations, extended through transitive composition and linear-identity substitution, uses a linear program to determine whether a candidate is already implied by known results. Candidates that pass are tested against a dataset of about 348,000 graphs assembled from the complete House of Graphs invariant export, all connected graphs with at most nine vertices, several named extremal graph families, and random graph models. Additional counterexample-search algorithms attack the remaining candidates. After several rounds on an HPC cluster, 6,522 conjectures had survived the refutation dataset, novelty filter, and every active search run. Among them were nontrivial relations involving the annihilation number and edge-cover number for bipartite and regular graphs; the authors prove these relations by hand. The later formalization stage deterministically converts each survivor into a Lean 4 statement skeleton. Candidate proofs are checked by the Lean kernel against a pinned version of mathlib4 and a custom invariant preamble. The pipeline connects two neural provers, DeepSeek-Prover-V2-671B served with vLLM and the Lean-specialized OProver-32B, to this independent kernel check. The end-to-end implementation has passed initial sanity checks, while the full pipeline is still running on the cluster.