AI-Driven Formal Proof Search

Sources#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• After Math
• Announcing FrontierMath Erdős
• AutoGraphForge: Towards Automated Graph Theory Discovery
• FLT: Anthropic has beaten me to it
• Learning to Discover Interesting Mathematics
• Long-horizon autoformalization of a core theorem underlying MIP* = RE
• OEIS Open: How many conjectures can language models turn into theorems?
• On the Navier–Stokes Millennium Prize Problem
• ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
• Quo Vadis? Scientific Discovery in the Age of Artificial Intelligence
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
• Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science
• When Does Structured Knowledge Help Neural Theorem Proving?

Summary#

The paradigm — demonstrated at research scale by Google DeepMind's AlphaProof Nexus (arXiv 2605.22763) — of using LLMs to generate proofs in a formal language (Lean) whose compiler mechanically verifies every logical step, then searching for a complete proof in a generate-and-verify loop. This converts the LLM's biggest liability for mathematics — hallucinated/subtly-wrong natural-language proofs that need expensive expert review — into a checkable artifact: a proof is correct iff Lean accepts it with no sorry and no disallowed axioms. The paper reports the first large-scale evaluation on open research problems, autonomously resolving 9/353 attempted Erdős problems and 44/492 OEIS conjectures, among other results.

Why formal, not natural language#

LLM natural-language proofs "contain subtle logical errors or hallucinations," and mistakes in unreviewed intermediate steps cascade, capping the complexity of what you can delegate. Formal languages fix this: in Lean, "definitions, theorems, and proofs are all mechanically verified code." The key reframing in the paper's discussion:

Formal verification can serve as a filter for determining which proofs merit human review.

So AI-driven formal proof search doesn't replace mathematicians — it triages. Experts review only what compiled, and within that, focus on the structure rather than re-verifying every line. This is Karpathy's verifiability thesis in its purest form: math+Lean is the maximally-verifiable domain, the compiler is the reward signal.

The framing contested (2026-09-21). De Toffoli and Duede (After Math, practitioner-opinion, no measurement) grant that Lean "secures certainty" but not that certainty is all a proof is for: the kernel ranks logical validity, not intelligibility, so "which proofs merit human review" gets everything that compiled, in no order. That is the filter's second blind spot (the first, below, is statement provenance; whether the certified statement is the intended one is Statement Drift). See Logical vs Intelligible Proof.

The competing branch (2026-09-21). Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science (Google Research + CMU, empirical) keeps proofs in natural-language LaTeX and checks them with a council of LLM falsifiers instead of a kernel: 71.0% on TCS-Bench (300 FOCS/STOC/SODA theorem tasks) and 46- and 75-page drafts, a research scale this paradigm has not matched. But the 71.0% is a reference-assisted model grader's verdict (">90% accuracy" on 100 expert labels, roughly ±30 problems of slack against a 3.0-point margin over one GPT-5.6 Pro call). Lean's 9-of-353 means a kernel accepted it; the council's 213-of-300 means a model that saw the answer key agreed. Detail on Many-Agent Proof Harnesses.

The proof-sketch interface#

The unit of work is a proof sketch: a Lean file with the target theorem, its dependencies (definitions, imports), and sorry in place of the proof. User-provided markers bound what the agent may edit — EVOLVE-BLOCK (introduce helper lemmas/definitions/steps) and EVOLVE-VALUE (change parameter expressions). The agent succeeds when it emits a sorry-free proof that SafeVerify accepts (compiles + no axiom injection like sorryAx). Optionally the mathematician supplies natural-language context and domain knowledge encoded in Lean. (See AlphaProof Nexus for the agent architectures that drive this loop.)

Compiler feedback as grounding#

The engine is the tight loop between generation and verification: the subagent edits via a search-replace tool, Lean compiles after each edit, and Lean's error message directs the next turn. The paper attributes the surprising strength of even its basic agent partly to "the power of compiler feedback in grounding LLM reasoning" (Agentic Loops Overtake Bespoke Systems). The verifier isn't just a final gate — it's a per-step teacher that keeps the model's reasoning anchored to ground truth.

Results (open research problems)#

• Erdős problems: 9/353 from the Formal Conjectures repo, including questions open since 1970/1996 and two open ~56 years; logged on Terence Tao's wiki of AI contributions to Erdős problems. Techniques span CRT + 3-AP-avoiding-set constructions (#12), inductive thinning exploiting Diophantine approximation $3^m\approx 4^k$ (#125), etc.
• OEIS: 44/492 open conjectures (with "test lemmas" verifying the first few sequence terms as a misformalization guard).
• Algebraic geometry: a ~15-year-open question on log-concavity of pure $O$-sequences (codim 3, type 2).
• Convex optimization: an exact $\mathcal{O}(1/t)$ rate for Anchored GDA — discovering a novel parameter schedule by marking the learning schedule as an EVOLVE-VALUE (proof and schedule searched jointly).
• Additive combinatorics: helped resolve #57 from Ben Green's list (formalized a candidate counterexample, agent proved it disproves the conjecture).
• Quantum optics (with Mario Krenn): monochromatic quantum-graph / high-dim GHZ-state existence for $N=d\in{4,6,10}$.
• Graph theory: a bipartite variant of the reconstruction conjecture; a 1996 conjecture from the Graffiti auto-conjecturing system (pointing toward an AI-conjecture→AI-proof loop).

The other half of the paradigm: scored benchmarks (ProofEvolve, 2026-08)#

The DeepMind results above are open research problems — an unscored denominator, where the right report is a list of what got solved. ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving (UVA + Meta AI, arXiv 2608.26334, empirical) supplies the complementary measurement: the same generate-and-verify paradigm run against competition benchmarks with a fixed denominator, so failures count. PutnamBench (pure-proof subset, 326 targets in its manifest), IMO-LeanProofBench (60), CombiBench (99). Best system: 71.2 / 53.3 / 49.0%, average 57.8%. Same frontier model with no search at all: 0.0 / 0.0 / 10.0%.

Three things this half of the paradigm makes visible that the research-problem half cannot.

The acceptance criterion, stated as a procedure. A solve must match the benchmark's statement, carry no placeholders, pass the kernel, and then be re-elaborated from scratch in a frozen environment with a restricted #print axioms check (only propext, Classical.choice, Quot.sound; native_decide excluded because it adds an axiom outside the kernel). Across 400+ re-verifications: 0 false positives. The native_decide exclusion in particular closes a verifier escape that a naive "Lean accepted it" check lets through (Kernel-Level Proof Auditing; protocol detail on Evolutionary Proof Search).

Benchmark leakage becomes the load-bearing human problem. To test whether a library of the prover's own verified proofs helps on held-out theorems, the authors had to show the held-out set was held out, and exact methods were not enough: after MinHash deduplication, five LLM judges screening for restatements "up to renaming or a change of constants" removed 256 of 1,000 evaluation theorems (25.6%), with a consequential, unvalidated threshold. So formal verification triages proofs perfectly and does nothing for statement provenance, which falls back on the LLM-judge machinery the compiler was supposed to replace. That is the filter's blind spot named precisely (screen detail on Evolutionary Proof Search).

The reachable boundary, characterized on open-weight models. A separate study runs the system on five open-weight models, eight configurations and a 485-target manifest at budget multipliers 0.25×–2× (the 1× profile: 12 model calls, 60 Lean calls, 400K tokens, 1,800s). Across all budgets and seeds they solve 11 distinct targets (4 Putnam, 7 CombiBench, none from IMO-LeanProofBench), the union rising 2 → 6 → 6 → 10 as budget quadruples twice. Every solved proof is 1–7 kernel-verified transitions and 1–23 model calls; several are one-lemma rewrites (Equiv.Perm.cycleType_inv, solved by all five models) or decide calls. The authors flag their own bias: the proof-state parser lacks the :mv, :mvd, :subst, :proj AST forms, unfinished runs grow with search depth, so means "may therefore be biased upward at larger budgets" and the curves are "descriptive search activity, not … unbiased estimates."

The full loop, wired end-to-end and not closed (AutoGraphForge, 2026-09)#

The Graffiti result above — a 1996 auto-conjectured statement proved in Lean — pointed at a loop where the machine also proposes the theorem. AutoGraphForge: Towards Automated Graph Theory Discovery (Ján Pastorek, Comenius University Bratislava, arXiv 2609.03478, empirical) is the first system in this corpus that builds all four stages — conjecture, refute, formalize, prove — into one pipeline and runs it at scale. It is the best available answer to "what does that pipeline look like," and the sharpest evidence about which stage is actually the bottleneck. See Automated Conjecturing for the generate-and-filter half; what belongs here is the formalize-and-prove half and the gap between them.

The architecture, in one line. A Graffiti3 generator over a small graph snapshot that grows only by counterexamples, a 559-relation novelty table decided by linear program, refutation against 348,207 graphs, parametric families, random models and six active counterexample searchers, then Lean 4 export to neural provers behind an independent kernel check: 1.22 CPU-years, 6,522 merged survivors (detail on Automated Conjecturing).

The formalization stage is the easy one, for a structural reason worth generalizing. Autoformalization is usually the error-prone step. Here it is a deterministic table lookup, because a TxGraffiti conjecture is already a formal object: each invariant column maps to a Lean name (zero_forcing_number ↦ G.zeroForcingNumber), each class predicate to a preamble hypothesis; binders are injected, both sides cast to ℝ, and any conjecture mentioning an unformalized invariant is skipped rather than guessed. The output is a sorry-terminated skeleton the kernel elaborates to a type-correct goal. Faithfulness holds by construction, with one trust assumption (the preamble definitions mean what they say, checked by hand by the author). Lesson: when the conjecturer emits typed objects rather than prose, misformalization does not arise, and the statement check is done once at the schema level instead of per theorem (Statement Drift).

The proving stage did not run, and that is the finding. Two open-weight provers are integrated, DeepSeek-Prover-V2-671B (vLLM, tensor-parallel across eight H200s) and the Lean-specialised OProver-32B, each usable whole-proof or in a compiler-feedback loop, with every candidate kernel-checked against pinned mathlib4 plus a custom GraphInvariants preamble and re-verified as a standalone .lean file. In total they have closed two trivial sanity-check inequalities over standard mathlib invariants, $\delta \le \Delta$ and $\omega \le n$ (both by OProver-32B), and zero of the 6,522 survivors. The paper says so ("we are explicit that the loop is not yet closed"), so the tier stays empirical for the first three stages while the fourth carries no evidence. Its two interesting survivors were proved by hand by the author (Automated Conjecturing).

The stated reason is vocabulary, not difficulty. The author's anticipated obstacle is that many survivors rest on invariants (zero forcing, total zero forcing, power domination, residue) defined only in his preamble and absent from the provers' training data. ProofEvolve's open-weight boundary is about proof depth on mathlib-native statements; this is a statement the kernel accepts and the prover has no prior for. If it holds, the reachable frontier of neural proof search is bounded by mathlib coverage of the vocabulary, and a conjecturer that ranges beyond mathlib's definitions generates targets its own prover cannot attack: a self-inflicted distribution shift built into the loop.

The third denominator: a fixed budget on curated open problems (FrontierMath Erdős, 2026-09)#

FrontierMath Erdős Benchmark (Epoch AI, Announcing FrontierMath Erdős, empirical) supplies a scored denominator of open research problems with the budget written into the score: 68 significant Erdős problems curated by Thomas Bloom, formalized in Lean (50 from Formal Conjectures, 18 by AI), checked by Comparator at $300 and 72 hours each. A pre-release GPT-6 Astra solves 2 of 68, four other frontier models none; off-protocol runs reach 5 of 68 for over $220,000. It prices formalization (Erdős problem 90: 18 pages of prose, 1.2 million lines of Lean, because of missing mathlib coverage), shows the low rate is not an artifact of DeepMind's easier item set (2.9% against 2.5%), and concentrates the statement-fidelity residual into the 18 AI-formalized statements (Statement Drift). Re-costing and the 9/353 reconciliation on FrontierMath Erdős Benchmark.

The fourth denominator, and the one that reprices all three (OEIS Open, 2026-08)#

OEIS Open (OEIS Open: How many conjectures can language models turn into theorems?, Adamczewski, Epoch AI, arXiv 2608.11941, empirical) breaks that low-rate agreement (9/353, 2/68, 0/6,522): Claude Opus 4.8 resolves 147 of 492 open OEIS conjectures in Lean, 30%, at a $50 cap, ten times the FrontierMath Erdős rate at a sixth of the budget. The items were selected as "not famous open problems" (451 of 492 sequences have no citing works), so "AI resolves X% of open problems" describes a selection procedure before it describes a model. It also brings the strictest verification protocol, the first measured disagreement between two Lean checkers (SafeVerify 147, Comparator 144), a ~40% disproof share, and misformalization left unreviewed on all 492 statements (Statement Drift). Detail on OEIS Open Benchmark.

The fifth denominator, where the items are easy and the verifier is what gets audited (2026-08)#

The four denominators above are open or research-level problems, and all four take "the kernel accepted it" as the fixed point. Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing (Bodla Krishna Vamshi and Haizhao Yang, University of Maryland, arXiv 2608.28639, 2026-08-11, empirical) inverts both: its items are closed competition problems (MiniF2F's 244 test theorems, PutnamBench's 659), and its second contribution audits the fixed point, finding that 31–44% of one released prover's PutnamBench "successes" depend on sorryAx (Kernel-Level Proof Auditing). The search design and its numbers stay here.

The compiler as a reward oracle, not a teacher. A generator, a decomposer (next natural-language subgoal) and a critic (0–100) share one frozen checkpoint under MCTS over natural-language proof plans. The Kimina Lean Server returns only how many of a node's attempts compiled, and no error text ever enters the generation context: context economy bought by degrading the verifier from per-step teacher to scalar oracle (Tree Search over Agent Trajectories (LATS)). At an exactly matched attempt budget it beats whole-proof sampling on every model (Goedel-Prover-V2-8B on MiniF2F: 87.1 ± 0.2% against 84.7 ± 0.1% at PAB@256) while using 32.84% fewer total tokens. Per-model results, the physics run and the ablations are on Agentic Loops Overtake Bespoke Systems.

The near-tie is the comparison that matters. A reproduction of Prover Agent, which does put compiler errors in context, reaches 86.2 ± 0.1% on MiniF2F at budget 260 against 87.1 ± 0.2% at PAB@256. Read against "compiler feedback as grounding" above, that is the most direct evidence in the corpus that the textual half of compiler feedback is close to free, on one benchmark, with the reproduction run by the party that wins it.

The caveat applies to every number on this page. Citing Gu et al. 2025, the same Goedel-Prover-V2-32B checkpoint measures 90% pass@64 on MiniF2F and 86 PutnamBench solves under Mathlib 4.9, and 80% and 75 under Mathlib 4.19. A prover figure is a joint statement about checkpoint, library pin, prompt template and verification check. ProofEvolve's 71.2% "PutnamBench" above is a 326-target pure-proof subset, not these 659, so the two are not comparable as written.

The claim that would break the ladder, and why it is not evidence yet (Navier–Stokes, 2026-09)#

OpenAI's Navier–Stokes Millennium Prize claim (On the Navier–Stokes Millennium Prize Problem, 2026-09-08, vendor-claim) sits above every empirical rate on this ladder and claims a Lean formalization in one clause: 17 hours by GPT‑6 Astra, not the internal model that found the proof. The post does not say what was formalized, which statement the Lean theorem states or who checked it against Clay's, the library version, or what axiom checks ran; the linked repository (github.com/openai/NavierStokesAndEuler) is not in this corpus. Against the one measured formalization of an AI-produced result (Erdős problem 90: 18 pages to 1.2 million lines, human-led), either an AI paid that tax in 17 hours or the artifacts differ in kind, and the statement's fidelity to the intended unforced problem is itself disputed (Statement Drift). Full treatment on The Navier–Stokes AI Claim.

Misformalization detection — an unexpected payoff#

Because the agent reasons against the formal statement, it surfaces errors in how problems were formalized. Examples: it found proofs by reading "density" as natural density, prompting corrections to "lower density" (#125) and "upper density" (#741(i)); it identified misformalizations in the literature. Failure modes also justify the formality: top sketches sometimes offloaded the core difficulty into a single sorry in a helper lemma restating the target, or cited "established" lemmas that were hallucinations — both caught precisely because end-to-end formal verification refuses to accept them. See Statement Drift.

Deepening human understanding#

The paper's stance: "the future of mathematics lies in human–machine partnership." Collaborators found that proof attempts enhanced their understanding even when the agent failed — formal sketches let experts focus on the unresolved subgoals rather than re-verifying the whole argument. This is Outsource Your Thinking, Not Your Understanding realized: the AI does the search; the mathematician's understanding is sharpened, not bypassed.

It is the corpus's strongest reply to the Logical vs Intelligible Proof objection, though it concerns the collaboration and the objection the artifact; see that page.

An outside survey's reading, and the community statement it surfaces (2026-09-23)#

Jedlička's survey (arXiv 2608.17970, practitioner-opinion) is secondary and vaguer than this page's primaries. It adds only pointers, none in this corpus: a footnote (accessed 2026-06-11) that the Erdős solutions were "not been yet published in a peer-reviewed journal"; Gowers calling OpenAI's disproof "a milestone"; Knuth's Claude Cycles endorsement of an unformalized collaboration; Ju et al.'s Lean-verified commutative-algebra resolution; and the Leiden Declaration on AI and Mathematics, a community statement on risks to "correctness, rigour, and standards of proof." Detail on Autonomous Scientific Discovery.

Choosing what to prove: interestingness-steered discovery (Patel et al., 2026-09)#

Every denominator above takes the target as given. Learning to Discover Interesting Mathematics (empirical, FAIR/NYU/CERMICS) closes a conjecture→prove loop in Lean: a conjecturer proposes, a Claude Code agent proves, and the ten proven statements with the highest proof-length-over-description-length ratio become the next round's premises. It closes where AutoGraphForge did not, but on mathlib-native vocabulary and with a permitted repair step that can weaken a statement until it is provable (Statement Drift). Outputs are far less contained in mathlib (30.6% against 91.9%); their usefulness is untested. Detail on Automated Conjecturing.

Does structured knowledge at inference time help? (Nabi, Vogl & Nabi, 2026-09)#

When Does Structured Knowledge Help Neural Theorem Proving? (empirical, Stanford, arXiv 2609.34460) ablates context supplied to a whole-proof prover with sequential error-guided refinement (pass@32 on miniF2F, 488 problems): none, an LLM-built knowledge graph of 364 mathlib theorems and definitions (9,434 typed edges), lexical mathlib declaration retrieval, or both, across matched Qwen3 and Goedel-Prover-V2 pairs at 8B and 32B plus Claude Sonnet 4.6. Weights beat context: Lean fine-tuning is worth 33-38 points in every mode (Goedel-8B 42.0% vs Qwen3-32B 12.7%), while no mode moves any model's aggregate more than 3 points. The sign is capability-conditioned: KG context helps Goedel-8B (+14, p=.029) and hurts Qwen3-32B (-14, p=.007); lexical retrieval never helps; every Sonnet delta is inside noise (p=.25-.31). The finding for the variance question is the per-problem oracle (union of the four modes): +23 for Sonnet (365 to 388), +18 to +36 for the rest, and on PutnamBench 34 to 45 (+32%). Read it as an upper bound, not a selector: the four runs are independent stochastic draws and no repeated prover_only run is reported, so the union mixes mode complementarity with plain run-to-run variance. At a matched 32-attempt budget (8 per mode) Sonnet's gain falls from +23 to +5 while the open models keep +17 to +27, and Sonnet's pass@k curves cross (with_mathlib +12 at pass@1, prover_only ahead at pass@3 to pass@20). Artifact: 10 and 28 KG-prompted Goedel-32B problems overflowed the 40,960-token window and were scored as failures (-3 becomes +1). Claude also built the graph and, as the evaluated model, selected its own context. Parse note: Table 8 (docling's lowest-confidence page) came out with two rows merged; reconciled by column sums against Table 9 and the prose (totals 438/421/426/429/483).

The formalization side of the frontier: FLT in 11 days (Buzzard on Anthropic, 2026-09)#

Kevin Buzzard's post on Anthropic's Lean formalization of Fermat's Last Theorem (FLT: Anthropic has beaten me to it, case-study) is a datum on the formalize known theory half of the frontier, not on discovery: over 13.4M lines in 11 days, which mathematically "tells us essentially nothing" because it follows the 1995 literature. Route, coverage, cost and library policy on Lean; the comparator run and his statement read on Kernel-Level Proof Auditing and Statement Drift.

Two research-level formalizations point the same way: Long-horizon autoformalization of a core theorem underlying MIP* = RE (case-study; MIP* = RE low-degree test, 126,367 Lean lines in 63 days, two statement and three error-budget corrections to the paper) and ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization (empirical; 33 stochastic-optimization developments, 28 published-source discrepancies). Formalization scales and audits; it still does not discover. Both are mainly evidence about Statement Drift.

Connections#

• Agent Harness Engineering — EVOLVE-BLOCK enforces invariants-not-implementations, a harness-engineering pattern
• Verification as the New Bottleneck — compiler-verified proofs are the purest case of verification as the gating step
• AlphaProof Nexus — the framework and agent architectures that implement the paradigm
• Lean — the proof assistant whose compiler provides the verification/grounding
• The Verifiability Thesis — math+Lean is the maximally-verifiable domain; the compiler is the reward signal
• Agentic Loops Overtake Bespoke Systems — the headline finding: a simple loop matched the bespoke system as LLMs improved
• Evolutionary Proof Search — the full-featured agent's population/Elo search mechanism, and the home of the kernel-grounded alternative (ProofEvolve's verified closure ρ plus a persistent Lean-checked schema library)
• Many-Agent Proof Harnesses — the branch that declines to formalize: natural-language research proofs checked by a council of model falsifiers instead of a kernel, at a research scale this paradigm has not matched (71.0% on 300 FOCS/STOC/SODA tasks, 46–75-page drafts) and with a correctness signal that is itself a model
• FrontierMath Erdős Benchmark — the third denominator: 68 curated open Erdős problems in Lean at a fixed $300/72h per attempt, where this paradigm's rate is 2/68 for one model and 0/68 for four others — plus the corpus's only measured price for the formalization burden (Erdős problem 90: 18 pages of prose, 1.2 million lines of Lean, cause stated as missing mathlib coverage)
• OEIS Open Benchmark — the fourth denominator and the one that reprices the other three: 492 OEIS conjectures selected to exclude famous open problems, $50 per attempt, 147/492 resolved where the FrontierMath Erdős protocol reaches 2/68 — so the headline rate on open problems is a property of the curation before it is a property of the model. Also the corpus's strictest verification protocol (three-axiom whitelist, native_decide excluded, three networkless containers) and its first measured disagreement between two independent Lean checkers (SafeVerify 147, Comparator 144)
• Tree Search over Agent Trajectories (LATS) — the same MCTS machinery one domain over, and the comparison that shows what a sound verifier buys a search: LATS sums an LLM judge with a sample-frequency term and must execute candidate actions to score them, while reward-oracle MCTS sums a critic with a compiler accept-count and probes for free
• Reward Hacking — the failure mode this paradigm is supposed to be immune to, and the one place it is not: the reward signal is the harness's summary of a compile run, not the kernel, and 31–44% of one prover's PutnamBench successes exploit the gap
• Kernel-Level Proof Auditing — the fixed point every denominator on this page rests on, finally audited: a compile-plus-sorry-scan harness accepts proofs that depend on sorryAx, voiding 4–19 of DeepSeek-Prover-V2-7B's PutnamBench successes per configuration (31–44% of them), while Goedel and Kimina come out clean across four benchmarks
• The Navier–Stokes AI Claim — the claim that would put this paradigm at the top of the ladder in one step, and the reason it cannot yet be counted: OpenAI says the Navier–Stokes blow-up proof was formalized and verified in Lean in 17 hours by GPT‑6 Astra, vendor-claim, with the repository and PDF linked but unexamined and no independent check anywhere
• Logical vs Intelligible Proof — the objection to this page's organizing framing: the kernel filters for logical validity and cannot rank intelligibility, so "which proofs merit human review" is answered with everything that compiled, in no order. practitioner-opinion, no measurement, and it concedes the paradigm secures certainty
• Terence Tao — the public register where this paradigm's Erdős solves are logged, and the host of the critique above
• Automated Conjecturing — the upstream stage that supplies the targets: forty years of Graffiti-lineage systems proposing invariant inequalities, their novelty-as-an-LP filter, and the measured triviality rate of what survives
• Agent Loop Pattern — the basic prover subagent is literally a "Ralph loop" (huntley2025ralph)
• Outsource Your Thinking, Not Your Understanding — formal sketches deepen mathematician understanding even on unsolved problems
• Client-Side Agent Optimization — solve-rate-vs-cost Pareto curves across agents (A/B/C/D) are the same cost/quality framing AgentOpt formalizes
• Scale-Dependent Prompt Sensitivity — smaller Gemini models solved nothing; capability is sharply scale-gated here (a hard threshold, not a smooth curve)
• Jagged Intelligence (Ghosts, Not Animals) — hallucinated "literature" lemmas are jaggedness; formal verification is the filter that catches it
• Autonomous Scientific Discovery — the wet-lab/life-sciences sibling: AI doing novel research without a Lean-style instant verifier, so the (slow, costly) experiment is the reward signal rather than a compiler
• Intelligence Explosion Dynamics — FunSearch/AlphaEvolve-style LLM-guided program search is concrete algorithmic self-improvement: AI finding novel constructions beyond its training distribution
• Transformative Creativity — DeepMind's report places new theorem-proving at Boden levels 1–2 (exploratory creativity within Lean's formal conceptual space)
• Deep Research Agents — the no-instant-verifier sibling in open-domain research: factual accuracy is its weakest axis precisely because there's no Lean-style compiler to ground each claim
• LLM-as-a-Judge — what open-domain research must fall back on absent a sound verifier; the contrast with the compiler's total verification here
• Optimizer–Evaluator Decoupling — the compiler is the limit case of that rule: an evaluator not merely independent of the prover but sound, which is why proof loops can run fully autonomous while agent eval-fix loops stay human-gated
• The Data Wall and the Validation Commons Are One Supply Constraint — this page reused as the corpus's clearest observed instance of a sub-task ordering: with Lean certifying every step, the residual human job is checking that the statement was formalized correctly, and the misformalization findings (natural vs lower density on #125, upper density on #741(i); difficulty offloaded into a restating sorry; hallucinated "established" lemmas) are what that residual looks like. So a domain's verifiable rung can be fully automated while its unverifiable rung stays load-bearing and human — which is the validation-commons ordering risk stated one level below where the labour literature puts it
• Latent Capability Overhang — OpenAI's disproof of the Erdős unit distance conjecture (informal, general-model, verified after the fact) is the test-time-compute sibling of this formally-verified work: same Erdős territory, opposite verification model — a general model steered at large budget vs. Lean certifying every step
• Post-Scarcity Macroeconomics — the sharpest test of the validation-commons argument: with Lean checking every step, the verifiable rung is fully automated and the residual human job moves to checking the formalization rather than the proof — the commons surviving one level down, at the sub-task boundary
• Anthropic — the lab behind the FLT formalization; see the 2026-09 FLT section (formalization at scale, not new theory)
• Statement Drift — the residual human job this page keeps naming (checking the statement, not the proof) as its own subject: four routes by which a kernel-accepted proof proves the wrong theorem, the one measured rate (61.8% compile, 11.2% aligned), and the FormalFlow and FLT statement audits

Open Questions#

• Successes cluster where Lean's mathlib is mature and problems decompose into tractable subgoals (combinatorics, convex optimization, number theory). What expands the frontier to problems needing new theory? Partially answered 2026-09-21 by AutoGraphForge: Towards Automated Graph Theory Discovery, which supplies a mechanism for the generating half and a warning about the proving half. Generating: a novelty filter that decides by linear program whether a candidate is implied by a convex combination of 559 tabled classical relations turns "is this new theory or a corollary?" into a decidable feasibility test with a non-negativity certificate, producing a queue of 6,522 statements provably not implied by the classical table — new-theory targets manufactured at scale rather than waited for. Warning: the same run exports those statements to Lean and has proved none of them, and the author's anticipated reason is that the invariants they quantify over (zero forcing, power domination, residue) are defined only in his own preamble and absent from the provers' training data. So the mechanism that reaches past existing theory is exactly the mechanism that leaves the prover out of distribution. Partial on two counts: that reason is an anticipation, not a measurement — the proving stage had not been run when the paper was written — and an LP over a hand-entered relation table certifies novelty relative to that table, not to the literature. Extended 2026-09-21 by Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science, whose answer is the uncomfortable one: drop the formal requirement. AutoGraphForge's bind was that reaching past existing theory puts the statement outside mathlib and therefore outside the prover's reach. Stellar Colosseum escapes the bind by never entering it — it works in natural-language LaTeX with a council of model falsifiers in place of a kernel, and reports five results answering questions raised in FOCS- and JMLR-published papers (a strong-coreset bound improved from ε^−p to ε^−2, a conditional condition-number barrier for sparse least squares, a near-closing m^{c/ε^{2−2δ}} embedding-dimension lower bound, a single-stage Hadamard quantizer, and a γ_{2,1} prefix-factorization lower bound within (log log n)^{3/2} of optimal). These are new theory, in the mathlib-hostile sense the AutoGraphForge note identifies, and the harness reached them. Two reasons this extends rather than answers. All five are self-authored companion arXiv preprints by three of the same six authors, none peer-reviewed and none formalized, and the paper itself declines to say how much human direction each received — quoting its own caveat about everyone else's discovery claims, "differences in human involvement, disclosure, and evaluation make it difficult to isolate the contribution of any one workflow component." And the escape is a trade, not a solution: what was bought is reach past mathlib's vocabulary, what was sold is the property this page exists to defend. The sharpened ask is now a third option neither source runs — post-hoc formalization of an unformalized result reached this way, which would measure whether the reach and the check can be recombined. Extended 2026-09-21 by Announcing FrontierMath Erdős, which is the closest thing to that third option anyone has run, and it prices it. The case is Erdős problem 90 — the unit distance conjecture, disproved by an OpenAI model in natural language and formalized afterwards by a separate human-led effort: 18 pages of prose, 1.2 million lines of Lean, and the stated reason is precisely this question's subject — the argument invokes a "deep" result that the standard library does not contain, so the paper could cite it while the formalization had to derive it from first principles. So the reach and the check can be recombined, once, at roughly 67,000 lines per page, with the cost driven by missing library vocabulary rather than by the difficulty of the new argument. That is a measured floor under the formalize-afterwards option, and it is why Epoch treats the burden as a limitation "of any Lean-based benchmark that asks AI systems to solve open problems" rather than of one system. Partial on three counts: it is a single instance, the formalization was human-led so it says nothing about an AI paying the tax, and it does not test whether the cost falls once the missing result is in the library — which is the falsifiable next step (formalize the deep prerequisite, then re-formalize the result and compare line counts). The same source also shows the frontier here is narrow rather than merely expensive: on 68 problems chosen for significance, one model reaches 2 and four reach none, against a curator's estimate that 3–5 problems of that calibre had ever been solved by AI. Extended a fourth time, 2026-09-21, by On the Navier–Stokes Millennium Prize Problem — the sharpest datum yet on this question and the weakest evidence on this page. OpenAI claims a Millennium-Prize-level result with a Lean formalization: a finite-time singularity for 3D Navier–Stokes, statements "C" and "D" of the Clay formulation, formalized and verified in a claimed 17 hours by GPT‑6 Astra after ~10,000 agents reached the proof in 88 hours. Taken at face value that is a direct answer — what expands the frontier to problems needing new theory is a model generation past the one that scores 2/68, run at a scale no benchmark protocol prices, with formalization as a separate downstream step by a weaker model rather than as the search substrate. Four reasons it extends rather than answers, and the tier is the first. It is vendor-claim — a first-party announcement about an unreleased internal model, disputed on priority, with no preprint, no independent Lean re-check and no refereed review in this corpus as of 2026-09-21. The formalization claim is one clause with none of the discipline the measured sources on this page publish: no axiom check, no statement review, no library version, and the linked repository was not fetched at ingest. It inverts rather than resolves the vocabulary bind this question keeps hitting — the corpus's one measured formalization of an AI-produced open-problem result ran 18 pages of prose to 1.2 million lines of Lean because the argument needed a "deep" result mathlib lacks, and fluid-PDE blow-up is not better covered; 17 hours against that is either a second-order capability jump or a different kind of artifact, and the post does not say which. And the search was steered by humans throughout — problem variants assigned per group, a mid-run pivot onto Navier–Stokes, the winning group guided by Codex-consolidated insights — so even granting the result, it says nothing about an autonomous route past existing theory. The falsifiable next step is now concrete and cheap: fetch the repository and the proof PDF and check whether the Lean statement is the Clay statement and the proof is sorry-free and axiom-clean. Definitional refinement, 2026-09-21, from After Math (practitioner-opinion, no measurement): De Toffoli and Duede's logical/intelligible split fixes what "new theory" has to mean for this question to be answerable at all — not a certified answer but a communicable argument other mathematicians can connect to existing knowledge and build on — which reclassifies all four extensions above as evidence about the certified half only, and leaves the third option this question keeps circling (reach plus check, recombined) still one property short of what is being asked for. Extended 2026-09-29 by Learning to Discover Interesting Mathematics (empirical), on the selection axis rather than the reach axis. Optimizing a proof-length-over-statement-length ratio cuts substantial or full mathlib overlap of generated statements from 91.9% to 30.6% and yields provable statements absent from mathlib, produced inside the formal setting with no natural-language escape. It does not show new theory: the statements are short mathlib-premise consequences, the evaluation cohort is selected on provability (with a permitted marginal-repair step), containment is judged by a Claude model, and the authors leave open whether the results help prove anything later. Still #oq/source. Extended 2026-09-29 by FLT: Anthropic has beaten me to it (case-study): the FLT repo shows the formalization half scaling (whole known proofs in days) while Buzzard states it adds no new mathematics, so it does not touch the new-theory half; it widens the gap between what is formalizable and what is discoverable.
• The agents inherit their LLMs' biases and show high search variance. How do you characterize and push the boundary of what's reachable? Partially answered 2026-09-21 by ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving, which supplies the first characterization half and almost none of the pushing half. Characterization: run one system across five open-weight models, eight configurations, three seeds and a 485-target manifest, and the reachable set is 11 distinct targets — 4 Putnam, 7 combinatorics, zero IMO-level — every one closed in 1–7 kernel-verified transitions, several of them single-lemma rewrites or decide calls. So the open-weight boundary is not "hard theorems reached slowly," it is "theorems one rewrite deep, and nothing beyond." On pushing: quadrupling the per-target budget twice moves the union of solved targets 2 → 10 out of 485, the authors disclose that their transition counts are biased upward at larger budgets by a parser-coverage artifact, and search structure rather than budget is what moves the frontier at the top end (0.0% → 71.2% on Putnam from adding search to the same frozen model). Still #oq/source: nothing here characterizes variance across seeds within a configuration at scale, and the strongest arm (Claude Opus 4.8) is never run over the budget ladder, so the boundary is mapped only where it is lowest. Extended 2026-09-21 by AutoGraphForge: Towards Automated Graph Theory Discovery along a boundary axis neither of the above touches: not proof depth but vocabulary. Its Lean export produces type-correct goals the kernel accepts, and its two integrated provers (DeepSeek-Prover-V2-671B, OProver-32B) have closed exactly two trivial mathlib-native inequalities and zero of the 6,522 exported conjectures, with the anticipated obstacle being that the conjectures' invariants exist only in a custom preamble. Nothing here is measured yet — the proving stage had not been run — so this sharpens the ask rather than answering it: a boundary characterization needs a vocabulary axis (mathlib-native versus preamble-only definitions) alongside the depth and budget axes already mapped. Extended again 2026-09-21 by Announcing FrontierMath Erdős, which supplies the first measurement instrument for this question rather than a fourth axis: a fixed budget applied to every item of a curated set of open problems. 68 significant Erdős problems, $300 and 72 hours per problem, one attempt each — a pre-release GPT-6 Astra closes 2, four other frontier models close none. The instrument's value is that it forces the boundary to be stated as reachable at a named price on a denominator nobody chose after the fact, which is exactly what the open-weight characterization above lacks and what the research-problem reports cannot give. It also supplies the first cost ladder on open problems: the same model, off-protocol, at larger budgets and repeated attempts, reaches 5 of 68 for over $220,000 against ~$20,000 for the scored run — with 269 attempts on the other 63 problems solving nothing. Read as a pushing result that is roughly two and a half orders of magnitude of spend for three extra problems, ~$67,000 marginal per problem against $172–$222 for the two the protocol found. Two structural details sharpen the ask further: the three extra solves each cost more than the $300 cap ($363, $405/$1,384, $617) and came from low per-attempt success rates (1/4, 2/5, 1/4), while the two the protocol found were solved on 7 of 7 and 5 of 5 attempts — so budget and per-draw reliability are separate axes and the protocol selects on both at once; and the same problem's solve cost varies 5.8× across attempts ($47 to $271 on problem 74), which is the search variance this question names, finally given a number. Still #oq/source: the ladder is uncontrolled (varied agent setups, varied attempt counts, one model), no other model was run above $300, and the announcement's own future-work line is the experiment that would settle it — how the solution count grows with budget per attempt and with number of attempts. That experiment was largely run three weeks earlier, 2026-08-12, by OEIS Open: How many conjectures can language models turn into theorems? — on a much easier denominator. OEIS Open plots, across eight runs and two budget caps, the fraction of conjectures resolved as a function of spend at the moment of resolution, and the answer is roughly linear in log-spend at about ten percentage points per tenfold increase, with no visible plateau at $200 — Claude Opus 4.8 goes 30% at a $50 cap to 39% at $200, and Epoch projects ~216 of 492 at $200 against the 147 measured at $50. Per-solve costs are $6–$10 on average with a $47 maximum, two orders of magnitude below the Erdős figures. Two axes this adds to the characterization half: a vocabulary axis held deliberately constant — integer-sequence conjectures were chosen because their statements need only integers and elementary operations rather than long chains of Mathlib definitions, which is the AutoGraphForge bottleneck removed by selection — and a model-diversity axis that comes out near-null, since the union of three labs' models at $50 is ~150 of 492 against 147 for the best single model, so the reachable set looks like a property of the problems. What it does not do is transfer: the slope is measured where the base rate is 30%, and FrontierMath Erdős's is 3%, so the ten-points-per-decade figure is a claim about the easy regime until someone runs the ladder on hard items. Still #oq/source. Extended 2026-09-29 by When Does Structured Knowledge Help Neural Theorem Proving? (empirical), on the variance axis. Choosing among four context modes per problem would lift Sonnet 4.6 by 6% on miniF2F but 28-32% on MathOlympiadBench and PutnamBench, so the reachable set on hard items is visibly run-dependent. What it cannot yet separate is context effect from sampling luck: no repeated no-context run is reported, and at matched attempts Sonnet's oracle gain shrinks from +23 to +5 problems. Still #oq/source; the missing control is same-mode, different-seed unions.
• The Graffiti result hints at closing the loop between AI conjecturing and AI proving. What does an end-to-end conjecture→formalize→prove pipeline look like? Partially answered 2026-09-21 by AutoGraphForge: Towards Automated Graph Theory Discovery — the shape half is now answered in full, the closure half is answered in the negative. Shape: a Graffiti3 generator over a ~2,860-graph snapshot that grows only by counterexamples to its own conjectures; a 559-relation novelty table deciding implication by linear program; refutation against 348,207 graphs plus parametric families, random models and six active searchers; a deterministic Lean 4 export (invariant column → Lean name, class predicate → preamble hypothesis) rather than an LLM autoformalizer; two open-weight neural provers behind an independent kernel check against pinned mathlib4. The pipeline is open-source and was run for 1.22 CPU-years, yielding 6,522 refutation-hardened survivors. The two non-obvious structural lessons are that autoformalization stops being the hard step once the conjecturer emits typed objects instead of prose, and that the bottleneck relocates entirely to proof search. Closure: the proving stage had not been run over the survivors — the provers had closed two trivial sanity-check inequalities and none of the 6,522, and the paper's own two interesting survivors were proved by hand. So the loop is wired, not closed, and stays #oq/source pending the completed run. Extended 2026-09-29 by Learning to Discover Interesting Mathematics — a second, differently-shaped pipeline whose prove stage does close. Conjecturer (RL-trained 27B, or Claude 4.6 at inference time) → semantic dedupe → Claude Code proof in Lean → promotion by interestingness → next round's premises; every retained statement is machine-verified, and statements are emitted directly as Lean types (no autoformalization step, matching the AutoGraphForge lesson). What it trades away: the conjectures live in mathlib's vocabulary, so the vocabulary bind that left AutoGraphForge at zero proved statements is absent by construction. Closure is shown; closure on new-vocabulary conjectures is not. Still #oq/source.

Sources#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving — arXiv 2608.26334, Ye et al. (University of Virginia + Meta AI), 2026-08-26, 28pp, empirical. Numbers above come from prose, figure captions and four tables re-read from pdftotext -layout against the local PDF; the docling parse's table-collapse flag on Appendix Table 4 is a header duplication, not damaged data (full note on Evolutionary Proof Search). Conflict of interest is mild but real — Meta AI publishing a system that beats five reproductions its own authors ran
• AutoGraphForge: Towards Automated Graph Theory Discovery — arXiv 2609.03478, Ján Pastorek (Comenius University in Bratislava), 2026-09-03, 17pp, submitted to ITAT 2026, empirical. Single author, workshop track, no independent replication — weigh the scale numbers (which are internally consistent and cheaply checkable) above the architectural claims, and treat the fourth stage as carrying no evidence at all: it is implemented and sanity-checked, not evaluated. Every figure cited above comes from prose or a pdftotext-verified table; the raw's Table 3 is a docling weld the ingest checks missed. Full source treatment, including the paper's one internal inconsistency, on Automated Conjecturing
• Announcing FrontierMath Erdős — Tom Adamczewski & Greg Burnham (Epoch AI), "Announcing FrontierMath Erdős", epoch.ai, 2026-09-01, ~2,250 words, empirical. A web article, not PDF-derived; both its tables are transcribed from HTML and were used as-is. Cited here for the 68-problem curation and the $300/72h protocol, the five-model score table, the off-protocol cost ladder, and the problem-90 formalization figures. Three bounds travel with every number: the only non-zero score belongs to a pre-release GPT-6 Astra that no third party can re-run; the companion paper is not in this corpus, so per-solution detail is unavailable; and the scored run is one attempt per problem, making 2/68 versus 0/68 a two-event difference (Fisher exact p ≈ 0.50 two-sided) that cannot by itself order the models. Full treatment on FrontierMath Erdős Benchmark
• On the Navier–Stokes Millennium Prize Problem — OpenAI (no byline), "On the Navier–Stokes Millennium Prize Problem", openai.com, 2026-09-08 with a 2026-09-10 update, ~1,900 words, vendor-claim (assigned; not upgradable without independent confirmation). Cited here only for the formalization claim, the 17-hour figure and its attribution to GPT‑6 Astra, and the 88-hour / ~10,000-agent search that preceded it. The proof PDF and the Lean repository are linked by the post and were not fetched, so nothing on this page about that artifact is an inspection of it. Total COI: OpenAI is claimant, producer, accused party, investigator and publisher in one unbylined document. Full treatment on The Navier–Stokes AI Claim
• Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science — arXiv 2609.15983, Lin, Woodruff, Deng, Mao, Zuo & Mirrokni (Google Research; Woodruff also CMU), v2 2026-09-15, 27pp, empirical. Cited here as the unformalized branch: §2.2 for the authors' own formal-versus-natural-language distinction (quoted verbatim), §6 for TCS-Bench and its reference-assisted model grader, §5.6 for the 46- and 75-page Knuth's-cycles drafts. All table rows reconciled against pdftotext -layout. Nothing in its mathematics arm is machine-checked — the correctness signal is a council of Gemini instances, and the headline grader is a model validated at ">90% accuracy" on 100 expert labels with no released agreement statistic. First-party Google evaluation of Gemini in which three of the six authors also co-wrote the benchmark. Full source treatment on Many-Agent Proof Harnesses
• After Math — Silvia De Toffoli (IUSS Pavia) and Eamon Duede (Princeton/Purdue), "After Math", guest post on Terence Tao's blog, 2026-09-12, ~2,000 words, practitioner-opinion. A philosophical argument with no measurements, no data and no protocol — cited here only for the logical/intelligible distinction and what it implies about the "filter for human review" framing, never as evidence about any system's behaviour. Its inline citations (Thurston 1994, Jaffe and Quinn 1993, Hales et al. 2009, Burgess and De Toffoli 2022, Avigad 2026, Tao 2026 arXiv 2608.16753) were not fetched; each is the authors' reading of a document this corpus does not hold. No lab affiliation and no result at stake, which is the source's main value; against that, one supporting citation is the first author's own and the venue is a blog. Full treatment on Logical vs Intelligible Proof
• OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski (Epoch AI), "OEIS Open: How many conjectures can language models turn into theorems?", arXiv 2608.11941, 2026-08-12, 27pp, empirical. Cited here for the 492-conjecture denominator and the $50/$200 caps, the 147/492 and 144/492 scores, the SafeVerify protocol and its Comparator cross-check, the proof/disproof split, and the item-set composition metadata. Single-author, same organization and same author as the FrontierMath Erdős announcement above, which is why the two are read as one instrument rather than as competitors. Every figure quoted here is from prose, a figure caption or a figure image; Table 1 (the only table, spread over 15 docling blocks) is reconciled in full against pdftotext -layout and is cited nowhere beyond its row count. Full treatment, including the paper's one internal arithmetic inconsistency (153 vs 147 + 44 − 35), on OEIS Open Benchmark
• Quo Vadis? Scientific Discovery in the Age of Artificial Intelligence — Petr O. Jedlička (Institute of Philosophy, Czech Academy of Sciences), Quo Vadis? Scientific Discovery in the Age of Artificial Intelligence, arXiv 2608.17970, 2026-08-18, 40pp, practitioner-opinion. Cited here for §5.1 (the mathematics/CS tour) and §7.1.1 (the Leiden Declaration) only, and only for what it adds: the footnote-21 peer-review status note, Gowers's assessment, Knuth's Claude Cycles endorsement, the Ju et al. commutative-algebra pointer, and the Leiden Declaration. Its restatements of AlphaProof Nexus, AlphaEvolve, FunSearch and the OpenAI Erdős results are secondary and vaguer than this page's primaries and were not carried. None of the five items above is in this corpus — each is a one- or two-sentence characterisation in a survey, and none was fetched. Parse note: PDF-derived (docling 2.126.0, MLX layout and table stages, 40pp, 0 tables, 2 pictures, confidence excellent); no table risk. §5.1's paragraph order is scrambled in the docling text flow (the OpenAI-result sentences are split and interleaved with the AlphaProof Nexus paragraph) — every claim quoted here was re-read from pdftotext -layout on (pp. 9–11). Full treatment on Autonomous Scientific Discovery
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing — Bodla Krishna Vamshi and Haizhao Yang (University of Maryland, College Park), arXiv 2608.28639, 2026-08-11, 14pp, preprint under review, empirical. Cited here for the three-role MCTS architecture and its reward definition, the PAB@B budget protocol, the MiniF2F/PutnamBench/PhysLeandata/LeanPhysBench results at matched budgets, the Prover Agent reproduction at budget 260, the token-efficiency figures, the temperature-decay and iteration-branching ablations, and the Implementation-details paragraph citing Gu et al. on Mathlib-version sensitivity. Weigh three things with it. It is a two-author unrefereed preprint with no third-party replication, and both baselines it beats are its own reproductions — including Prover Agent, the one arm that could have beaten it. Every model is 7–8B open-weight, so nothing here speaks to frontier-scale provers. And the paper's own denominators are closed competition problems, which makes it the only source on this page not measuring open-problem resolution — it is carried here for the search design, the matched-budget discipline and the audit, not as a fifth data point about research mathematics. Parse note: PDF-derived (docling 2.126.0, MLX layout + table stages, 14pp, 11 tables, 1 picture, confidence excellent). Tables 3 and 5 were reconstructed at ingest after docling dropped whole sub-rows, and Tables 2/4/6/7/9 repaired; every figure quoted above was re-confirmed against pdftotext -layout -f 6 -l 9 on the local PDF and against the prose. Full source treatment on wiki/sources.md; the axiom-audit half on Kernel-Level Proof Auditing
• Learning to Discover Interesting Mathematics — Patel et al. (FAIR @ Meta, NYU, CERMICS), arXiv 2609.28603, 2026-09-23, 27pp, empirical. Cited for the closed interestingness-promotion loop and the containment result. Every quoted figure is from prose or a figure caption; the docling table-collapse/table-split-row warnings fall on the appendix TOC and hyperparameter tables, none cited. All judging and proving is by Claude models. Full treatment on Automated Conjecturing
• When Does Structured Knowledge Help Neural Theorem Proving? — Nabi, Vogl & Nabi (Stanford), arXiv 2609.34460, 2026-09-28, 30pp, empirical. Cited for the inference-time context ablation and the per-problem oracle only; MathKG construction and the unevaluated open-ended mode are not used.
• FLT: Anthropic has beaten me to it — Kevin Buzzard, "FLT: Anthropic has beaten me to it", Xena Project blog, 2026-09-04, ~1,000-word post plus 23 selected comments, case-study (raw says practitioner-opinion). Cited for the FLT formalization datum only; cost figures are unverified commenter claims.
• Long-horizon autoformalization of a core theorem underlying MIP* = RE — Lu, Deng, Zhu & Ji, arXiv 2609.19814, 2026-09-17, case-study. Cited for the one sentence above only; full treatment on Kernel-Level Proof Auditing.
• FrontierMath Erdős — Adamczewski & Bloom, arXiv 2609.25050, 2026-09-06, empirical. Refines this page's 9/353 Erdős figure (nine statements span seven problems, four unambiguously resolved); detail on FrontierMath Erdős Benchmark.
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization — Han et al., arXiv 2608.29270, 2026-08-29, empirical. Statement-fidelity measurement for Lean autoformalization (61.8% compile, 11.2% semantically aligned); see Kernel-Level Proof Auditing.
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization — Wang, Li & Yuan, arXiv 2609.34960, empirical. Cited for the one sentence above only; full treatment on Kernel-Level Proof Auditing.