Automated Conjecturing

Sources#

Summary#

The half of machine mathematical discovery that runs before AI-Driven Formal Proof Search: a system holds a table of examples with computed invariants, and proposes statements — almost always inequalities between invariants, sometimes sufficient conditions for a graph class — that hold on every row. It is a forty-year-old field with almost no LLM content in it. Fajtlowicz's Graffiti (1988), DeLaViña's Graffiti.pc, the AutoGraphiX / GraPHedron programme, Davila's TxGraffiti and The Optimist, Larson's Dalmatian-based Conjecturing and Graffiti 3, and the polyhedral PHOEG system are all pre-neural search over a grammar of invariant expressions. Their conjectures have become real theorems; DeepMind's proof-search agent closed a 1996 Graffiti conjecture in Lean (Advancing Mathematics Research with AI-Driven Formal Proof Search), which is the datum that made the conjecture→proof loop look imminent.

The defining difficulty is not generating candidates — that is combinatorially easy — but deciding which ones are worth anyone's time. Everything interesting in the field is filtering.

Three paradigms for searching the space of inequalities#

Algebraic expression trees (Graffiti, Conjecturing): build candidates as rooted trees of invariants combined by unary and binary operations (sums, products, square roots) and enumerate by exhaustive or heuristic tree search.
Linear / mixed-integer programming (TxGraffiti, The Optimist, Graffiti 3): solve an optimisation model over a precomputed tabular dataset, minimising the distance between a target invariant and a linear combination of others. The tightest bound is found, not enumerated.
Polyhedral / geometric (GraPHedron, PHOEG, and now Graffiti 3): embed each example as a point in invariant space and read conjectures off the facets of the convex hull. This yields the complete set of optimal linear inequalities over those invariants and makes optimality a geometric certificate rather than a heuristic.

The geometry is also the core difficulty: infinitely many halfspaces are true on a finite table, but only the facets — tight on at least one extremal object — carry information, and no single inequality is "the best."

The five failure modes#

The reusable frame, from AutoGraphForge: Towards Automated Graph Theory Discovery §1. Anyone running such a system meets all five:

False in general — holds on every example in the dataset yet fails on a graph the dataset lacks.
True but known — already in the literature.
True but trivial — the "avalanche of triviality."
Monster conjecture — one candidate overfits the table by accumulating terms and constants: $\alpha \le 0.31\Delta + 0.42\nu - 0.07m + 1.8$.
"Counterexample" to a well-established theorem — which essentially always means a bug in an invariant routine, not a discovery.

Modes 1 and 5 are about trust (a holding inequality and a found counterexample are only as reliable as the invariant code); modes 2 and 3 are about novelty. They are mitigated by three different mechanisms — adversarial counterexample search, a novelty filter, and selection heuristics — and as the numbers below show, mitigated is not eliminated.

Novelty restated as a decidable linear program#

The sharpest technical idea in this corpus's coverage of the field. Instead of asking a human or a model whether a candidate $f \le R(g)$ is new, ask whether it is implied by a convex combination of tabled theorems: assign non-negative weights $w_j$ summing to 1 over known bounds $f \le B_j(g)$ and test whether $R(g) - \sum_j w_j B_j(g) \ge 0$ everywhere. Non-negativity is certified by writing that difference identically as

$$R(g) - \sum_j w_j B_j(g) ;=; \sum_i s_i,(g_i - L_i) ;+; \sum_k \mu_k E_k(g) ;+; t$$

with safe lower bounds $g_i \ge L_i$, class identities $E_k(g) = 0$, a constant slack $t \ge 0$, and free multipliers $\mu_k$. Because the invariants are treated as independent symbolic variables, matching coefficients turns this into LP feasibility. A feasible solution is a proof of redundancy; the candidate is flagged a known rediscovery and excluded from the novel set but retained as a soundness check.

Two details make it sound rather than merely convenient. A bound is admitted into the aggregate only if it holds over the candidate's entire hypothesis class or a superclass of it, and a class identity only if the candidate's class is that class or a subclass — so a bipartite-only theorem cannot be used to dismiss a candidate about all graphs. Class inclusions (tree ⊂ bipartite, cubic ⊂ regular) propagate bounds downward automatically. Equalities are flagged known when both directions are implied; necessary conditions are handled by contraposition. And the one place the method refuses to generalize is instructive: a sufficient condition concluding a class membership ($A \Rightarrow C$) is checked only against a hand-curated table of textbook characterizations, because a rare invariant equality can agree with a class on every test graph by coincidence — so data-mined characterizations are inadmissible and all other such candidates are conservatively left novel.

The table itself is small and human-authored: 559 classical, folklore and trivial relations (Whitney's $\kappa \le \lambda \le \delta$, König's $\nu = \tau$ on bipartite graphs, Gallai's $n = \alpha + \tau$, and so on), after closing the simple $f \le g$ relations under transitivity.

Selection heuristics from the Graffiti lineage#

Three, all pre-neural, all still doing the work:

Dalmatian (dominance, Fajtlowicz; revisited by Larson & Van Cleemput): discard a candidate whenever an accepted conjecture is never weaker and sometimes strictly tighter.
Morgan: drop a bound asserted on a restricted class when the same bound holds on a superclass.
Touch: rank by how often the bound is sharp on the dataset. High touch means the conjecture traces the extremal boundary closely — and it is the ranking used to decide which survivors a human reads first.

Refutation: where the fitness signal is graded, and brute force wins#

Conjecturing's companion stage is counterexample search, and it has a property that proof search conspicuously lacks: a natural continuous objective. For a candidate $f(G) \le R(g)(G)$ the margin is $f(G) - R(g)(G)$, positive exactly on a refuting graph and larger for a more decisive one. Every backend is just a different way of maximising it, so the whole stochastic-search toolbox applies directly — SMT encoding (z3), variable-neighbourhood search, linear cross-entropy, MCTS, simulated annealing, and a deep-RL edge-selection policy in the Wagner/RLGT lineage. Compare Evolutionary Proof Search, where the verdict is binary and the entire design problem is manufacturing a gradient that does not exist.

The empirical result is the surprise, and it points the other way from the sophistication. Across AutoGraphForge's five HPC partitions, the six search algorithms together contributed only 1–22 counterexamples per round, while a precomputed static table of 348,207 graphs supplied 500–790 witnesses in round 1 alone. In the single-pass baseline, of 1,249 refutations, 865 came from the extremal families, 217 from random models and 161 from the House of Graphs export — the remainder from the search algorithms. The author flags the caveat himself: one run, stochastic searchers at default un-tuned hyperparameters, so it is not a verdict on the methods. But as a systems result it is the same shape as Agentic Loops Overtake Bespoke Systems — cheap exhaustive lookup did the work the elaborate machinery was built for.

What a run at scale actually produces#

The numbers below are from AutoGraphForge: Towards Automated Graph Theory Discovery, a single generate-refute campaign on a 256-core-per-node HPC cluster costing 1.22 CPU-years (≈0.37 for the loop itself, ≈0.85 for one-time precomputation of 59 invariants over the refutation dataset — the NP-hard independence/domination/zero-forcing ILPs dominate).

Generation runs on a tiny table; refutation runs on a huge one. Conjectures are generated over a snapshot $T$ of a few thousand graphs that grows only by counterexamples to its own conjectures (337 TxGraffiti "expressive" graphs → 1,554 → 2,860 across successive runs), while refutation tests against 348,207 graphs (28,859 House of Graphs + 273,192 = every connected graph on 2 ≤ n ≤ 9 + 46,156 special families). Generating over the full dataset would be prohibitive, and a small counterexample-hardened core suffices.
The loop terminates. Per-round new witnesses collapse — ~500–790 in round 1 (a 20–28% expansion of $T$), ~40–160 in round 2, ~3–20 in round 3 — and four of five partitions hit a fixed point (a round adding zero witnesses) at round 5. The decline is not monotone: partition 1 rebounded to 24 and 25 witnesses in rounds 4 and ≥5 before terminating at round 9.
Survivors: 8,281 raw across the five partitions, reduced to 6,522 in two stages — 1,413 refuted by a witness another partition had found but this one never saw (each partition grows its own hard seed in isolation), and 346 cross-partition duplicate Sophie conditions.
Composition: 2,677 class-conditioned inequalities + 3,845 Sophie sufficient/necessary conditions. 33 survivors are flagged by the novelty filter as rediscoveries of classical results (Gallai's $\tau = n - \alpha$, König–Egerváry, the perfect-graph identity $\alpha = \theta$, rad $\le \alpha$) — presented, correctly, as a soundness check rather than a discovery: the generator recombining invariants into known relations is the design working.

The triviality problem, measured#

This is the part worth carrying, because it is the first number in this corpus attached to the "avalanche of triviality." The top 100 survivors by touch count were classified automatically from the pipeline's own novelty table, subsumption lattice and support statistics:

Category	Count
Rediscovery recognised by the novelty filter	49
Subsumed by a stronger survivor	2
Decorative hypothesis (the class does no work)	1
Promising, universal (no class hypothesis)	28
Promising, class-conditioned	20

So just over half of the highest-ranked survivors are triage successes in the pessimistic sense — the system already knows they are not news — and the residual 48 are merely "not known to us to be trivial or false." The author refuses to report a "probably false" bucket on the grounds that every item survived the full 348,207-graph battery, so there is no evidence of falsity to report. Even after a 559-relation filter and three ranking heuristics, the honest yield of a top-100 read is under half. Failure mode 3 is not solved; it is quantified.

(Reconciliation note: §4.1's prose says "essentially none of the surviving novel candidates is an unconditioned inequality," which does not sit easily beside the 28 "universal (no class hypothesis)" entries in this table — both re-read from pdftotext -layout. The class-conditioned claim is the one the paper's own worked examples support; see the Sources note.)

The same problem on the human-authored side, measured differently (OEIS Open, 2026-08)#

The audit above is of a machine's conjecture queue. OEIS OPEN (OEIS Open: How many conjectures can language models turn into theorems?, Epoch AI, arXiv 2608.11941, empirical) supplies the comparison case: 492 conjectures proposed by humans and approved by OEIS volunteer editors, selected down from 2,649 open OEIS conjectures by a Gemini prompt asking for problems "non-trivial, mathematically interesting, not famous open problems, and good candidates for automated theorem-proving." Epoch then measured the composition of what that filter produced, and the shape is recognisably this page's:

Attention. 47% of the conjectures sit on OEIS entries with no links or references at all, and 451 of the 492 sequences have zero citing works in OpenAlex. The zero-citation bin is both the largest (n=230 of 492) and the highest-scoring for every model. So the queue is overwhelmingly composed of statements nobody has written about, and those are the ones that fall first.
Concentration. 127 distinct proposers, but the prolific conjecturer Zhi-Wei Sun proposed 37% of the set — and his are the hardest (~16% solved by at least one of three runs, against 41% for the 176 conjectures from the 116 long-tail proposers). A single human conjecture-generator dominates a curated corpus the way this page's machine generators dominate theirs.
Falsity, at scale. Between 37% and 48% of the conjectures AI resolves here are resolved by disproof. This page's audit deliberately reports no "probably false" bucket because its survivors cleared a 348,207-graph refutation battery; OEIS conjectures cleared no such battery, and the result is that nearly half of the resolvable ones are simply wrong. That is failure mode 1 (false) surviving human editorial review at a rate the machine pipelines' refutation stage would not permit — evidence that AutoGraphForge's brute-force refutation table is doing real work that human review does not replicate.

What this does not supply is the triviality count: nobody classified the 153 resolved OEIS conjectures as rediscovery, subsumed or decorative, so the honest-yield question this page quantifies for machine queues stays unmeasured for the human one. The attention proxies are the nearest available stand-in, and Epoch says so — "attention to a sequence is only a proxy for attention to a conjecture about that sequence."

What came out that was actually mathematics#

Two class-conditioned survivors relating the annihilation number $a(G)$ (largest $k$ such that the $k$ smallest degrees sum to at most $m$) and the edge-cover number ec$(G)$, forming a complementary pair where the bound flips direction:

$$G \text{ bipartite} \Rightarrow \mathrm{ec}(G) \le a(G) \qquad\text{(rank 91 by touch, touch 922)}$$ $$G \text{ regular} \Rightarrow a(G) \le \mathrm{ec}(G) \qquad\text{(rank 177, touch 589)}$$

Neither is in the novelty table; both are provable in a few lines by combining classical results. (1) falls out of Gallai's two identities plus König's theorem — on a bipartite graph ec $= n - \nu = n - \tau = \alpha$, and Pepper's $\alpha \le a$ finishes it. (2) is a direct computation: an $r$-regular graph has $a(G) = \lfloor n/2 \rfloor$ and ec$(G) = n - \nu \ge n/2$, with equality exactly when $G$ has a perfect matching — so the bound is tight for bridgeless cubic graphs by Petersen's theorem. The cubic specialisation the system also produced (rank 453) is correctly flagged subsumed, since cubic ⊂ regular.

The author's own verdict is the right one: "Neither of these is a deep new theorem." What they demonstrate is that the pipeline's output reduces to short human-checkable arguments rather than to noise — a statement about the tractability of the survivors, not about their depth. Note also how they were proved: by hand, on paper, by the author — not by the two neural provers the same system integrates (AI-Driven Formal Proof Search carries that gap).

The conceptual space is printed#

Automated conjecturing is the cleanest available case of Boden level-2 exploratory creativity, because unlike AlphaGo or AlphaFold the conceptual space is not inferred from outputs — it is written down and auditable. Here it is a linear grammar of halfspaces over 45 numeric target invariants, with 16 boolean predicates (14 graph-class flags plus two derived order thresholds) available as hypotheses, filtered against 559 named theorems. Nothing in the pipeline can propose an invariant that is not already a column, or a class that is not already a predicate. See Transformative Creativity for why that matters and Autonomous Scientific Discovery for the wet-lab sibling where the space is not printed.

Evidence note#

The scale results above are empirical and the arithmetic is internally consistent, but the source is a single-author submission to a regional workshop track (ITAT 2026), with no independent replication, no external validation of the counterexample-search comparison, and an LLM used as a coding and experimentation assistant (declared). Invariant computation is the one thing independently checked: GraphCalc against House of Graphs on 2,500 graphs, zero mismatches on every shared invariant, plus a networkx cross-validation unit test before every run — which is exactly the guard failure mode 5 demands.

A learned, measurable interestingness signal (Patel et al., 2026-09)#

Every source above filters conjectures by validity or novelty (refuted, implied by a table, not yet proved). Learning to Discover Interesting Mathematics (FAIR/NYU/CERMICS, arXiv 2609.28603, empirical) is the first in the corpus to define and optimize a filter for interestingness, entirely inside Lean's mathlib.

The metric. Conditional interestingness I(T|P) = 100 · V(T|P) / L(T|P): proof lines over description length, where V is the proof length given premises P and L counts the statement plus every definition needed to state it that the premises do not already supply. Dividing by L is what stops conjunctions padding the score (a conjunction of n unrelated theorems has difficulty O(n) but interestingness O(1)). Over all mathlib (empty premises, I0) the ordering is intuitive: algebraic identities at the bottom, Fermat's Last Theorem for exponent 3 near the top.
Utility check. U0(T) = |direct users| · V(T|∅), lines saved across the library if T is free. Spearman ρ = 0.756 between I0 and U0 on mathlib, excluding declarations with U0 = 0. Two caveats the paper does not flag: V sits in both quantities, so some correlation is built in, and the exclusion removes the theorems nobody uses. The claim that "few statements, if any, have high utility without high interestingness" is the more informative half.
A learned estimator. Because proving every candidate is expensive, a Qwen3.6-27B is GRPO-trained (350 steps, ~110k prompts built by "premise expansion" over mathlib's dependency DAG) to predict V. On 4,615 held-out prompts (Figure 1, viewed): MAE 20.2 proof lines against 31.0 for GPT-5.5 and 34.3 for Claude Opus 4.6, Spearman 0.912 against 0.776 and 0.815; all three underestimate long proofs, and GPT-5.5 collapses in the longest bin. (4,615 = 5,538 validation prompts minus the 923 unlabeled base_drop rows, so the appendix and the main text agree.)
Optimizing it. A 75-step GRPO run rewards the conjecturer with 0.25 + log(1 + I/100), with parse failures at −0.5, non-compiling or unrelated statements at −0.25 and statements closed by rfl/simp/tauto-class automation at 0. Scored on ground truth (each statement proved by a Claude Code + Opus 4.6 agent, 20 proven per model per area, 8 areas, 160 per model), mean I rises from 1.76 (base) to 7.58, above base in all eight areas (2.10× combinatorics to 8.72× number theory) and above prompted Claude Opus 4.6. An LLM judge (Opus 4.6) scores 30.6% of the trained model's statements as substantially or fully contained in mathlib (rubric levels 4–5) against 91.9% for the base and 92.5% for Claude.
Inference-time promotion loop. Claude 4.6 proposes 400 statements from 20 premises, a semantic filter dedupes, Claude Code proves, and the ten highest-I proven statements join the premises for the next round. Against retain-all, random and longest-proof promotion, interestingness pruning is ranked most interesting first in 60% of 100 blinded four-way comparisons (proof length 19%, no pruning 13%, random 8%) and its cohorts score 3.40 on quality versus 2.40–2.60. Longest-proof pruning being worse is the evidence that the ratio carries the gain, not proof length. Through round 6 the promoted statements form reusable theorem graphs (Figures 6 and 9), with showcased runs in graph theory, algebra, measure/probability and number theory.

How this reads against the rest of the page. AutoGraphForge's filter is a decidable logical test against a hand-entered table; this one is a scalar computed from the formal library itself, needs no table, and is not tied to graph invariants (the paper's own contrast with Graffiti/TxGraffiti). And the proof stage is closed here — every statement retained was proved by an agent — which the AutoGraphForge pipeline did not manage. But the measure is a library-relative complexity ratio, not the logical/intelligible property of Logical vs Intelligible Proof: a statement can be short to state and long to prove because mathlib lacks the API, not because there is an idea. Weigh the headline numbers against four things. The judges are Claude models, and Claude is also the baseline conjecturer, the loop's conjecturer, filter and prover, so the 92.5% containment score is one Claude grading another. Statements enter the ground-truth cohort only if a prover agent can prove them, with a permitted "marginal repair" (added hypothesis, weakened conclusion, Jaccard ≥ 0.70), so the cohort is selected on provability. Proof lines are a stylistic quantity (the authors note aesop/grind trade length for runtime). And the paper's own closing admits it is "not yet clear if the new theorems are also useful for proving future results", so downstream utility of generated theorems, the property the metric is validated against on mathlib, is untested. Unreconciled inconsistency: the main text runs the loop for 6 rounds (Figure 7) while Appendix D's Table 1 averages "ten rounds", and Appendix D gives 80 premises in P0 where the Figure 9 caption says 240.

Connections#

OEIS Open Benchmark — this page's problems measured on a human-authored queue: 492 open OEIS conjectures past volunteer editorial review, 47% on entries with no references, 37% from one prolific conjecturer, and 37–48% of the AI-resolved ones resolved by disproof — failure mode 1 surviving human review at a rate a refutation battery would not permit. The triviality bucket this page quantifies is the one it does not measure
AI-Driven Formal Proof Search — the downstream half; AutoGraphForge is the first system to wire both together, and the place the wiring is shown not to carry load yet
Evolutionary Proof Search — the mirror image: refutation search has the graded margin fitness that proof search has to manufacture
Agentic Loops Overtake Bespoke Systems — the brute-table-beats-six-searchers result is the same shape one level down, in counterexample search rather than proof search
Transformative Creativity — the printed conceptual space makes the Boden level checkable by reading rather than inferring
Autonomous Scientific Discovery — hypothesis generation without a wet lab; the same discovery loop where the verifier is instant and the space is enumerable
The Verifiability Thesis — conjecturing sits outside the verifiable region: a candidate's truth is undecidable by the machinery that generated it, which is why refutation and proof are separate stages
Logical vs Intelligible Proof — the distinction that says what an unimpliedness certificate is and is not: a logical property of the statement, decided by linear program, and silent on whether the statement is one a mathematician can connect to anything. The interestingness question this page ends on is the intelligibility question one stage before any proof exists
Lean — the target language the surviving conjectures are exported into; mathlib is also the ground truth from which the proof-length interestingness metric and its estimator are built
AlphaProof Nexus — the proof-search framework that closed a 1996 Graffiti conjecture, the result that motivated closing the loop
Statement Drift — the prove-stage risk in closed conjecture loops: Patel et al.'s repair step lets a statement be weakened until it is provable, while AutoGraphForge's typed Lean export makes drift impossible by construction

Open Questions#

The novelty filter is only as good as its 559 hand-entered relations, and 49 of the top 100 survivors were rediscoveries anyway. Does the novel-survivor count fall by an order of magnitude as the table is expanded toward a real literature, or does the rediscovery rate stay flat because the generator's grammar is the binding constraint?
The 6,522 survivors are, by construction, statements not implied by the classical table. Is that a usable definition of mathematically interesting, or does a queue of thousands of unimplied class-conditioned inequalities just relocate the triage problem from the machine to the reader? Partially answered 2026-09-21 by After Math (practitioner-opinion, an argument with no measurement, and one that never mentions this system). De Toffoli and Duede's logical/intelligible split supplies the missing half of the definition this question is probing. "Not implied by a convex combination of 559 tabled relations" is a logical property — decidable, certificate-bearing, and by construction indifferent to whether anyone can say what makes the statement true or connect it to anything. What mathematicians want from a result, on their account, is the other property: ideas they can grasp, communicate, connect with existing knowledge and build on. Read through that split the answer to this question's disjunction is the second branch — an unimpliedness certificate is a filter, not a criterion of interest, so the triage does relocate to the reader, and the page's own top-100 audit (49 rediscoveries, 2 subsumed, 1 inert hypothesis) is what that looks like in practice. It stays partial and stays #oq/now for two reasons: the source is an opinion piece about a different system, so this is the wiki applying its distinction rather than the authors ruling on this queue; and intelligibility has no instrument anywhere in the corpus, so the reformulated criterion is no more measurable than the one it replaces. Extended 2026-09-29 by Learning to Discover Interesting Mathematics (empirical), which supplies the first measured alternative to unimpliedness as a definition: proof length over statement-plus-definition length, validated against downstream library utility on mathlib (ρ = 0.756) and shown to steer a model toward statements 4.3× more interesting on that metric and far less contained in mathlib (30.6% vs 91.9%). It is an instrument for the logical-side quantity "hard to prove relative to how it is stated", not for intelligibility, and its validation set is mathlib rather than generated conjectures, so the question stays partial.
Sufficient conditions concluding class membership are admitted as known only against a hand-curated characterization table, because coincidental agreement on a finite dataset is not a theorem. Can that judgement be automated at all — or is "is this a characterization or an accident?" the irreducibly human residue of the conjecturing stage?
Proof-length-over-description-length is validated as a proxy for downstream utility only on existing mathlib theorems. Do statements a conjecturer optimizes for it, kept in a self-expanding library, actually shorten later proofs, or does the optimizer find statements that are hard to prove only because mathlib lacks the API, with no reuse value?

Sources#

AutoGraphForge: Towards Automated Graph Theory Discovery — AutoGraphForge: Towards Automated Graph Theory Discovery, Ján Pastorek (Comenius University in Bratislava), arXiv 2609.03478, 2026-09-03, 17pp, submitted to ITAT 2026, empirical. Single author, workshop track, code at github.com/JanPastorek/AutoGraphForge. Parse warning, in this wiki's convention: the raw is docling-derived and verify.py reported no table warnings, but Table 3 (backend hyperparameters) is welded — five backend rows collapsed into a single row with all five labels in one cell (cross_entropy vns mcts sa rlgt-RL) and all five settings strings concatenated in the other. table-collapse missed it; pdftotext -layout shows five clean rows. Tables 1 and 2 were re-read cell-for-cell from pdftotext -layout and match the prose (Table 1's Surv. column sums to the stated 8,281; Table 2 sums to 100); their docling rendering carries only cosmetic digit splatter (1, 762). Both figures were viewed: image_000000 is a CC-BY badge, not a figure — the real Figure 1 is image_000001. Internal inconsistency flagged, unresolved: §4.1's "essentially none of the surviving novel candidates is an unconditioned inequality" versus Table 2's 28 "Promising, universal (no class hypothesis)" among the top 100, which §4.2 says are ranked among the 2,677 class-conditioned survivors. Both readings verified against the PDF; the paper does not reconcile them.
Advancing Mathematics Research with AI-Driven Formal Proof Search — cited here only for the 1996 Graffiti conjecture closed in Lean, the datum that frames conjecturing as the upstream stage of a loop rather than a standalone field.
After Math — De Toffoli & Duede, "After Math", guest post on Terence Tao's blog, 2026-09-12, practitioner-opinion. Cited on this page for one thing only: the logical/intelligible distinction, used to reframe the "is unimpliedness a definition of interesting?" question. The post is about OpenAI's Navier–Stokes announcement and never mentions conjecturing, AutoGraphForge or graph theory — the application is this wiki's. No measurement of any kind. Full treatment on Logical vs Intelligible Proof
OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski (Epoch AI), arXiv 2608.11941, 2026-08-12, 27pp, empirical. Cited here for the composition of a human-authored open-conjecture queue: the 2,649 → 500 → 492 selection and its prompt, the citation and proposer metadata (Figures 4 and 5, viewed; their bins sum to 492 exactly, which is the arithmetic check), and the proof/disproof split from Figure 1. Epoch states the metadata's own limit — citations to a sequence are a proxy for attention to a conjecture about it. No triviality classification of the resolved set exists. Full treatment on OEIS Open Benchmark
Learning to Discover Interesting Mathematics — Patel, Rammal, Hayat, Munos & Kempe (FAIR @ Meta, NYU, CERMICS), arXiv 2609.28603, 2026-09-23, 27pp, empirical. Cited for the interestingness and utility definitions, the 27B difficulty predictor (Figure 1, viewed: MAE 20.2/31.0/34.3, ρ 0.912/0.776/0.815), the 1.76 → 7.58 mean-interestingness shift, the 91.9% → 30.6% mathlib-containment drop, and the promotion-rule ablation (Tables 3 and 4 read cell-for-cell; row counts match the prose). Parse warning: the table-collapse flags fall on the appendix table of contents and the two hyperparameter tables (B.2.2, C.1.3), which docling welded into two-column value cells; none of their values is cited here (step counts come from prose). The table-split-row orphans '18', '19', '26' are TOC page numbers. Authors are the lab that trained the estimator; all judging and proving is by Claude models. Full treatment in the section above and on wiki/sources.md