Formal Math, in order.

Open questions 39 open

• Agentic Loops Overtake Bespoke Systems2 open
  • WaitThe bespoke advantage is dated "for now." What's the next model generation's verdict — does the evolutionary/AlphaProof apparatus survive on any problems, or fully collapse to a cost line? Partially answered 2026-09-21, by analogy rather than directly — stellar colosseum many agent harness math tcs does not test the evolutionary/AlphaProof apparatus or run in Lean, so it cannot close this. What it does supply is the first instance of the predicted collapse happening within a single paper's own baseline column, one model generation on: a 27-page bespoke many-agent harness reaches 54.0% on research-level TCS proofs with Gemini 3.1 Pro, a model-side thinking mode on the same family reaches 52.0% with no harness at all, and a stronger model's plain single call (GPT-5.6 Pro max) reaches 68.0% — 14 points above the harness. The mechanism is the one predicted here, with a twist worth recording: the capability was absorbed not by a better loop but by test-time compute moving inside the model, which is a route this page did not anticipate. Three reasons it stays #oq/wait: different apparatus, different verifier (model council, not a kernel), and the comparison is cross-vendor rather than the same system re-run on a newer model. The trigger event is unchanged — the AlphaProof/evolutionary system re-run on a next-generation LLM against the same nine Erdős problems. Extended 2026-09-21 by openai navier stokes millennium prize solution, and the extension is a warning rather than a datum. The next model generation arrived, and what the lab holding it built around it was more apparatus, not less: ~10,000 concurrent agents in communicating groups, per-group problem variants, a mid-run model swap, a separate model consolidating insights across groups, and a Lean pass at the end. So the first observation of frontier-model-plus-bespoke-apparatus at the new generation points the opposite way from this question's expectation — though it cannot be scored, because the announcement reports no baseline, no ablation and no comparison of any kind, and it is vendor-claim about an unreleased model. Two readings stay live and this source separates them: the apparatus may still be buying capability at the frontier, or it may be the cheapest way to spend a weekend's compute when nobody is measuring efficiency. The trigger event is unchanged, and this adds a second one worth watching — any lab publishing a same-problem comparison between its many-agent apparatus and a single long-running agent on the newest model. Partially answered 2026-09-23 by oeis open conjectures theorems, from the other side of the comparison. Nobody re-ran the apparatus on a newer model; instead a third party ran a three-tool loop on newer models against the apparatus's own 492-conjecture OEIS item set at a $50 cap, and the apparatus's 44/492 became the bar in someone else's figure at 147/492 — a 3.3× gap at matched average cost per resolved conjecture (~$10 either way, from the apparatus authors' own correspondence). Read against this question that is the collapse it anticipates, one generation on and on 492 items rather than nine. It stays #oq/wait because the apparatus itself was never re-run: Gemini 3.1 Pro against Opus 4.8 and GPT-5.5 is a two-to-three-month model gap, so the result cannot separate "the apparatus stopped paying" from "the newer model would have made the apparatus better too." The trigger event is unchanged.
  • SourceDoes the "simple loop + verifier beats bespoke system" result hold only where the verifier is perfect (Lean), or also in noisy-verifier domains (tests, LLM-judge councils)? Partially answered 2026-09-21 — and the answer arrived from an unexpected direction. proofevolve neuro symbolic evolution formal atp says nothing about noisy verifiers; everything in it runs against the Lean kernel. What it does is falsify the question's premise inside the perfect-verifier case: run the comparison at matched, tight per-target budget with the base model frozen and a plain ReAct loop scores 25.7% average against 57.8% for the bespoke evolutionary system, with the intermediate systems ordered monotonically between them. So the result does not even hold unconditionally where the verifier is perfect — it holds where the verifier is perfect and budget is effectively uncapped. The noisy-verifier half is still open, and is now a sharper ask: a budget-matched loop-vs-bespoke sweep in a domain whose verifier is a test suite or a judge council, which would separate "structure buys sample efficiency" from "structure buys robustness to a lying verifier." Extended the same day by stellar colosseum many agent harness math tcs, which supplies the noisy-verifier domain and still not the loop arm. Stellar Colosseum is a bespoke many-agent harness whose entire correctness signal is model-generated — adversarial falsifiers, per-section reviewers and a global verifier, with no formal check anywhere in its mathematics arm — so the "perfect verifier" premise is finally removed. Result: against an unscaffolded single call on the same frozen model, the elaborate structure is worth +23.7 points (30.3% → 54.0% on 300 research-level FOCS/STOC/SODA theorem tasks). So a noisy verifier does not by itself destroy the value of bespoke structure; the ProofEvolve direction holds outside Lean. Two things keep this partial and keep the tag at #oq/source. First, the loop arm is missing entirely — every comparator in the paper is a direct model call, there is no ReAct-style loop, no best-of-N control, and the paper publishes no token count, call count, wall-clock or dollar figure at all, so the budget axis the reconciliation above turns on cannot even be located. The authors concede it in future work: compute-matched evaluation "would be needed to distinguish improved allocation from simply using more inference." Second, in the other direction the same table shows a stronger model's plain single call (68.0%) beating the whole harness (54.0%), which is a harness-shrinkage datum rather than a loop-beats-bespoke datum and does not substitute for one. The ask is now precise: run a plain loop and the bespoke harness at a stated, matched call budget on the same model with a judge-council verifier. A third source arrives 2026-09-21 with the missing budget and the same missing arm (openai navier stokes millennium prize solution, vendor-claim): a ~10,000-agent apparatus over 88 hours, 2.7 million inter-agent messages and ~130 billion output tokens, ending in a Lean verification — so the verifier is back to perfect and the budget is published in full, and there is still no loop arm, no single-agent arm and no ablation. Worth recording because it makes the pattern a property of the field rather than of one paper: across three sources in one month, two verifier regimes and two labs, nobody has run the comparator, and the one party asked about it directly says the experiment has not been done. Partially answered 2026-09-23 — somebody ran a comparator, in the perfect-verifier regime, and it came out null. oeis open conjectures theorems runs base ReAct against Inspect's deepagent (subagent delegation, persistent memory, a todo-list tool, a longer system prompt) on the same model, the same 100-conjecture LITE subset, the same Lean/SafeVerify gate and the same $200 cap: 39/39, 36/41, 29/29 across Claude Opus 4.8, GPT-5.5 and Gemini 3.5 Flash. A 476,000-paper arXiv literature arm is equally flat (39/37/28). So bespoke agentic affordance buys nothing at matched budget with a sound verifier, which is the opposite sign from ProofEvolve's bespoke search machinery at matched budget — and the distinction between the two kinds of structure is the useful thing this adds. Two reasons it stays #oq/source: the verifier is still perfect, so the noisy-verifier half of the question is untouched; and the arms are matched on dollars rather than on calls or tokens, so a DeepAgent arm that spends its $200 on subagent overhead rather than on proof attempts is not distinguishable from one whose affordances simply do not help.
• AI-Driven Formal Proof Search3 open
  • SourceSuccesses 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 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 many agent harness math tcs, 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 epoch frontiermath erdos announcement, 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 openai navier stokes millennium prize solution — 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 de toffoli duede tao guest post (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.
  • SourceThe 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 formal atp, 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 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 epoch frontiermath erdos announcement, 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 conjectures 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 structured knowledge 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.
  • SourceThe 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 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.
• Automated Conjecturing4 open
  • The novelty filter is only as good as its 559 hand-entered relations, and 49 of the top 100
  • The 6,522 survivors are, by construction, statements not implied by the classical table. Is that a
  • Sufficient conditions concluding class membership are admitted as known only against a hand-curated
  • Proof-length-over-description-length is validated as a proxy for downstream utility only on
• Evolutionary Proof Search2 open
  • SourceThe LLM-critic fitness is itself an unverified heuristic atop a verified substrate. How often does the Elo ranking mislead the search vs. the cost of computing it? Partially answered 2026-09-21 by proofevolve neuro symbolic evolution formal atp, and the partiality matters. ProofEvolve builds the same kind of search with the heuristic removed — fitness is verified closure ρ, computed for free from kernel-accepted edges, with no rater fleet, no Plackett–Luce posterior and no Gibbs sampling — and beats five agentic baselines on the same frozen base model at matched budget (57.8% average against LEAP's 50.5% and Hilbert's 45.9%). So the unverified ranking is demonstrably not necessary, and its compute is demonstrably avoidable. What remains unanswered is the question as literally posed: nobody has run LLM-critic Elo and verified closure as the only varied factor inside one system, so the misleading rate is still unmeasured, and ρ's own blind spot — it cannot see strategy clarity or novelty, only discharged obligations — is untested in the other direction. Note also that this is comparative evidence across two different provers, not a test of DeepMind's system.
  • SourceHyperparameters ($c=0.2$, top-64, $P=7$) were "chosen empirically." How sensitive is the result to them, and do they transfer across mathematical domains? Partially answered 2026-09-21, on the transfer half only. ProofEvolve's per-benchmark margins over the same runner-up swing from +16.6 points on IMO-LeanProofBench to −1.0 on CombiBench, and its operator ablation splits the same benchmark by difficulty and finds every operator contributing roughly three times more on the Advanced split than the Basic one (full system 22/30 Basic vs 10/30 Advanced; without decomposition 9/30 and 2/30). So in this family of systems the configuration does not transfer uniformly across mathematical domains — combinatorics, where proofs rest on an explicit construction rather than an assembly of lemmas, is where the elaborate search stops paying. The sensitivity half is untouched: ProofEvolve reports no value for its own archive temperature τ or descriptor binning and runs no sweep over them, and the one hyperparameter it does sweep (retrieval depth K = 8/16/32/64) moves the outcome non-monotonically inside the noise band. Related evidence, 2026-09-29, structured knowledge neural theorem proving (empirical; not an evolutionary system): a fixed context-augmentation configuration does not transfer across models either, since knowledge-graph context flips from +14 solves (Goedel-8B) to -14 (Qwen3-32B) on the same miniF2F set, with only per-problem selection recovering value. It says nothing about $c$, top-K or $P$ specifically, so the sensitivity half stays untouched.
• FrontierMath Erdős Benchmark4 open
  • SourceDo the 18 AI-produced formalizations survive expert review — and are any of the five solved problems among them? Epoch states the 18 passed only its own initial review by self-described non-Lean-experts, with expert review "in process," and never says which subset the solves came from. A misformalization inside the solved set would turn a headline into an artifact; one outside it would leave the score intact and the denominator soft. Extended 2026-09-29 by flt anthropic has beaten me to it (case-study): a contrasting case where the statement was expert-read: Buzzard states he checked that the FLT statement matches the theorem, and that this is the one part the machine cannot check. Says nothing about Epoch's 18. Extended 2026-09-29 by long horizon autoformalization mip star re (case-study): the second contrasting case, and the first where expert review changed the formal statement: a coauthor of the source paper audited the top-level theorem and gap resolutions, and 25 gap notes led to corrections of two errors in the published statement and three in the error budget (final bound preserved). It also shows why unreviewed AI formalizations are risky: agents produced tautological aliases and conclusion-inlined hypotheses that compiled. Still nothing on Epoch's 18. Partially answered 2026-09-29 by frontiermath erdos (empirical): the statements were not left unreviewed — Bloom reviewed each of the 18 autoformalized conjectures (17 problems) for fidelity to the original problem — but he is the curator, not a Lean-formalization auditor, and the paper does not say whether any of the five solved problems is among the 18. Two questions remain: an independent Lean-expert review, and the provenance of the five solves.
  • SourceHow does the solve count actually grow with budget per attempt and with number of attempts? Epoch names this as future work and its own off-protocol data is the uncontrolled version: 5 solved, ~~269~~ 172 fruitless attempts (paper's recount), >$220,000 against ~$20,000. The falsifiable form: run the same model on the same 68 at $300 / $1,000 / $3,000 with k attempts each and check whether coverage climbs log-linearly, as it does on closed benchmarks with a verifier, or hits a ceiling set by which problems are reachable at all. Partially answered 2026-09-23 by oeis open conjectures theorems, on a different item set. OEIS Open runs exactly this measurement — solve rate against per-sample spend at the moment of solve, across eight runs, two budget caps and five models — and finds it roughly linear in log-spend at about ten percentage points per tenfold increase, with no visible plateau at the $200 cap; within one model, Claude Opus 4.8 goes 30% at $50 to 39% at $200, and Epoch projects ~216 of 492 at $200 against 147 measured at $50. So on some open-problem set the curve is log-linear rather than ceilinged, which is the first evidence either way. Three reasons it stays open here: the base rate is 30% rather than 3%, so the slope is measured entirely in a regime this benchmark never reaches; the spend axis is reconstructed from when a solve happened inside a capped run rather than from independent runs at different caps, and the paper flags the bias itself (agents are told their budget, which may change their behaviour); and the number-of-attempts axis is untouched — OEIS Open is one run per model per configuration, so the k-attempts half of this question has still never been run.
  • WaitDoes the post-hoc contamination correction keep scores comparable, or does the usable denominator shrink faster than capability grows? Epoch's plan is to filter problems solved before a model's cutoff and compare on the remainder. Trigger event: the first model run against this set after solutions to some of the 68 have been published.
  • WaitDo the five AI proofs survive human digestion, and are #1 and #571 genuinely new? The paper says the proofs are kernel-verified but "not yet digested", and that the relation of the #571 proof to existing work "will take some time". Falsifiable by the human write-up the authors promise, or by a literature match. Trigger: the first refereed exposition of any of the five.
• Kernel-Level Proof Auditing6 open
  • SourceEvery published MiniF2F and PutnamBench number in this corpus that was not gated on an axiom whitelist rests on a compile-plus-sorry-scan pipeline. How many of them move under an exhaustive #print axioms re-audit? Answerable directly and cheaply for any prover that released its accepted proof artifacts — run the check and publish audited-versus-unaudited pairs, the way this paper does. Extended 2026-09-29 by flt anthropic has beaten me to it: a counter-example on the strong side (a 13.4M-line artifact passed comparator), not evidence about the unaudited benchmark numbers.
  • Source#print axioms catches escapes that route through an axiom; SafeVerify's kernel-type and definition-body matching catches proving a different or trivialized statement. Is the union of the two complete, or is there a class of verifier escape that compiles, passes the three-axiom whitelist, matches the target's kernel type, and is still not a proof of the intended theorem? Partially answered 2026-09-29 by long horizon autoformalization mip star re (case-study): yes, and it is the statement itself. The comparator matches the formal statement to a registered target, but only human audit (a coauthor of the source paper unfolding definitions to primitives) certifies that the target is the paper's theorem; and inside a project, tautological aliases, vacuous witnesses and conclusion-inlined hypotheses all compile and stay inside the three axioms, so the union is complete for escapes of the proof and silent on drift of the statement. Not settled: this is one project's catalogue, not a rate. Extended 2026-09-29 by emergent cheating whistleblowing research swarms (case-study): a field instance of the redefinition class. local notation placed before the theorem changes the elaborated statement while its source bytes stay identical, which #print axioms would pass and elaborated-statement identity would reject. It supports the ladder rather than finding a new escape. It also surfaces an adjacent gap: on answer-slot problems the solver supplies part of the statement, and an answer defined as the target itself (Target ↔ Target) needs a separate constraint on the answer term.
  • SourceExploit-dependent successes rise 2.75× under search at PAB@32 (11 against 4) while the exploit rate among successes stays roughly flat (31–44% across both procedures and both budgets). Does a verifier-guided search actively select for the exploit once the budget is large enough — the reward signal cannot distinguish a sorryAx success from a real one, so the search should climb toward it — or does the rate stay flat because the exploit is just another way to be right-shaped? Falsifiable by extending this paper's own audited/unaudited pairs across the full PAB ladder.
  • SourceDoes the ~82% misalignment among compiling outputs survive when the target statement is given, not generated? ShadowBench measures agents that write both statement and proof from informal text. Benchmarks that fix the statement (OEIS Open, FrontierMath Erdős) sidestep that failure but inherit the benchmark author's formalization; the falsifiable test is to run SA-Pass-style forward and backward checks over those benchmarks' own reference statements.
  • SourceDoes ProofLoom's construction-time Judge survive an independent statement audit? The Judge and the 43-case ablation are the authors' own, with an LLM among the labellers. The falsifiable test: run SA-Pass-style forward and backward implication checks, or an expert unfolding like FormalFlow's, over the released source-facing statements of a sample of the 32 released developments, and count any weaker than the source.
  • SourceDo the authors of the 25 selected-version discrepancies acknowledge them? Three (Category B) already have author corrections in later versions or errata; the 25 do not. Author errata or replies for SAM A17, SPIDER A21 or MARS A23 would settle whether these are source errors or interpretation differences.
• Logical vs Intelligible Proof3 open
  • Is intelligibility operationalizable at all, or does it stay a philosopher's distinction? The
  • Where an AI-produced open-problem result exists as both a prose argument and a formalization, which
  • De Toffoli and Duede concede the first argument has a shelf life: future systems are "likely to produce
• Many-Agent Proof Harnesses5 open
  • SourceThe 71.0% headline rests on a reference-assisted model grader validated at ">90% accuracy" on 100 expert-labeled proofs — roughly ±30 problems of slack on a 300-task benchmark, against a 9-problem margin over a direct GPT-5.6 Pro (max) call. Does an expert re-grade of the 213 accepted proofs preserve the ordering, or does the harness's entire advantage over a single strong call dissolve into grader noise? Contrast 2026-09-29: long horizon autoformalization mip star re (case-study) shows the alternative grader design: kernel acceptance plus a human statement audit, with review agents demoted to a filter. It does not answer this question (different task, no benchmark), but it prices the alternative: 21,651 review comments and a paper author's time. Scope sharpened 2026-09-21 by after math de toffoli duede tao guest post (practitioner-opinion): an expert re-grade would replace one judgement of validity with a better one, and would leave untested the property De Toffoli and Duede argue a proof is actually for — whether a reader can say what makes the theorem true and use it. So even the strongest available answer to this question certifies less than the benchmark's framing implies, and the missing instrument is not a better grader but a different measurement.
  • SourceEvery TCS-Bench comparator is a single direct call; the paper names the missing control itself ("compute-matched evaluation would be needed to distinguish improved allocation from simply using more inference"). At a matched total model-call budget, how much of the 30.3% → 54.0% lift survives against plain best-of-N on the same model with the same critique selector on top? Partially answered 2026-09-23, in miniature and in the other verifier regime. oeis open conjectures theorems runs the matched control this question asks for — same model, same task set, same dollar budget, varying only the harness — on the smallest many-agent affordance set there is (Inspect's deepagent: subagent delegation, persistent memory, todo list, longer system prompt) against a three-tool ReAct loop, and the lift is zero (39/39, 36/41, 29/29 on 100 conjectures at a $200 cap). So a matched control is runnable and, at that scale, the structure does not survive it. Three reasons this does not close the question: the scale is two orders of magnitude below Colosseum's tree; the verifier is Lean rather than a council, which is the condition this branch exists to relax; and the matching is on dollars rather than on model calls, so it cannot separate "the affordances do not help" from "the affordances spend the budget on themselves."
  • WaitNone of the five §5 results has cleared peer review or a formal check, and all are self-authored companion preprints. Do any of arXiv 2608.26047, 2608.02588, 2607.20393, 2608.02564 or 2608.08238 get accepted at a refereed venue, formalized, or corrected?
  • SourceWould enforcement tools have stopped the swarm's exploit? The research-swarm authors claim that with direct norm-enforcement tools the collective "could have autonomously neutralized the cheats". Those tools would include voting on proofs, rejecting library entries and banning agents. They also say both behaviours "reliably reproduced" across runs, with no numbers. Falsifiable by rerunning the same 100-agent, 71-problem setup with (a) a sanction or removal tool and (b) a static grader, and reporting the fraudulent-solve count and the cohort split per run.
  • SourceWhat produced the 24% whistleblower share: the model, the conference framing, or the escalation tool? The paper credits three features: transparent channels, a scientific-conference frame, and a feedback endpoint. METR's investigation of the covert board found 3 to 6 agents considering a human alert and none acting on it, with no such tool, frame or model in common. Falsifiable by an ablation that removes the framing and the feedback tool one at a time in the same swarm.
• OEIS Open Benchmark3 open
  • SourceIs the resolvable subset a fixed property of the problems? The union of three $50 runs across three labs' models is ~150 of 492, against 147 for the best single model — i.e. model diversity adds about three conjectures. Falsifiable directly: publish the per-conjecture solve matrix and report pairwise overlaps, or run one model k times and compare the k-run union to the three-model union. If model diversity really buys nothing, the benchmark measures problem difficulty alone and pass@k reporting on it is meaningless.
  • SourceDoes the literature null survive a retrieval-shaped test? 476,000 arXiv papers changed no model's score, but the agent had only bash over a LaTeX source tree and no retrieval index, and 47% of the conjectures sit on OEIS entries with no references at all. Separating "the answers are not in the literature" from "the agent cannot find them" needs one of: a keyword/embedding index over the same corpus, or a solve-rate split between conjectures whose sequences do and do not have citing works under the literature arm specifically.
  • SourceHow many of the 153 resolved conjectures were misformalized? Epoch performed no validation and expects some to be wrong; Tsoukalas et al. reviewed their 44 and found none. Every accepted proof is public, so this is answerable by the same human review at roughly 3.5× the effort — and it is the one check that would turn the 30% from an upper bound into a measurement. Extended 2026-09-29 by shadowbench semantic alignment autoformalization (empirical): no count, but a prior and a method. On a different object (agents generating statements from informal text, not a benchmark author formalizing them) the best system compiles 61.8% and is aligned 11.2%, and 65 of 110 compiling outputs fail both implication directions; a benchmark whose statements are given avoids that generation failure but not the author's formalization error (ShadowBench itself withdrew one problem for a faulty reference statement and excluded 31% of ProofNet for known faulty references). The method transfers: forward and backward checks against independently formalized shadow theorems can be run on the 153 resolved statements.
• Statement Drift2 open
  • SourceIs FormalFlow's 1 → 63 flagged-statement curve typical of agent-built formal libraries? It is one project, and the count went to zero only when the scanner became blocking. The falsifiable test is to run a comparable proof-debt scan (conclusion-shaped hypotheses, circular dependencies, unproved helper obligations) over another agent-built repository with public history, such as the FLT repository or ProofLoom's released developments, and report flagged statements per accepted line over time.
  • SourceDoes the human statement read scale with the artifact, or stay roughly constant? Buzzard read FLT's statement, Bloom reviewed 18 autoformalized conjectures, and a FormalFlow coauthor unfolded definitions to primitives. None of them reports the time spent or what was checked beyond the top-level theorem. If it stays constant, it becomes the cheap fixed cost of trusting a 13.4M-line proof. If it grows with the auxiliary definitions the statement depends on (ShadowBench finds alignment failing where auxiliary declarations accumulate), it becomes the bottleneck. Settled by any source that times a statement audit against statement and dependency size.
• The Navier–Stokes AI Claim5 open
  • SourceDoes the linked Lean artifact (github.com/openai/NavierStokesAndEuler) actually contain a sorry-free, axiom-clean proof of a statement that a competent third party agrees is the Clay statement "C"? The post asserts a formalization and publishes none of the discipline; the repo and the two PDFs exist and are not in this corpus. Falsifiable by fetching and inspecting them — the cheapest open question on this page and the one everything else rests on. Partially answered 2026-09-29 (did openai solve the wrong navier stokes problem, practitioner-opinion): on the statement half, Scientific American reports that the result does resolve Clay's original formulation via its forcing option "C", which is what the post claims; but it also reports that the community reads the forced statement as a loophole rather than the intended problem, so "a competent third party agrees it is the Clay statement" now depends on which reading of Clay is meant. The sorry/axiom half is untouched. Scope sharpened 2026-09-21 by after math de toffoli duede tao guest post (practitioner-opinion): a clean repository would settle this question in full and would still leave the result an answer rather than a solution on De Toffoli and Duede's account — the kernel certifies deductive validity by a procedure that "does not itself require understanding," so nothing in the repository can show that the proof conveys why the theorem is true. Worth holding when reading a future "verified" headline: what the check buys is certainty, which is less than the announcement's framing implies and more than nothing. Contrast 2026-09-29 (flt anthropic has beaten me to it, case-study): the Anthropic FLT repo, also a vendor artifact, was compiled and run through comparator by an outside expert (Buzzard) and passed; no equivalent third-party check of the Navier-Stokes repo is reported here.
  • WaitDoes the result survive independent verification? (Trigger events, any of: a refereed publication or arXiv preprint of the proof; an independent Lean re-check by a party outside OpenAI; a statement from the Clay Mathematics Institute; or a published refutation.) As of 2026-09-21 none has occurred, which is why the tier is vendor-claim.
  • WaitHow does the priority and influence dispute resolve — specifically, does any party outside OpenAI ever get to check the claim that Buckmaster's Codex prompts "could not have influenced the system in any way, including through training"? The denial rests on an investigation by the accused party, and hardened from "cannot rule out" to "could not have" in two days. (Trigger: an external audit, a disclosure of the training-data provenance, or a statement from Alpöge or Buckmaster accepting or rejecting the account.)
  • WaitIs the unforced 3D Navier–Stokes problem in fact resolved differently, i.e. does blow-up occur without an external force, or does the forced-only scenario the article raises turn out to be the truth? (Trigger: a blow-up construction for the unforced equations, or a proof of global regularity there; also whether Clay revises the statement.)
  • SourceWhat exactly does arXiv 2609.20803 prove, and does its "cannot extend" result cover only OpenAI's ansatz or every method of the forced-blow-up programme? Falsifiable by fetching and reading the paper, which this corpus reports only through Scientific American.