From June to November 2026, AI labs and AI-assisted authors made 56 public mathematics claims that this census found. 38 come with a formal artefact; 34 have been decided here, from the claimants' own bytes, with no code shared with them. Where a proof was replayed, the kernels accepted it. What fails, when something fails, is the step between the formal object and the headline. The gaps come first.
Each claim is filed under every kind of gap it shows. A claim can show several.
| kind of gap | claims | what it means |
|---|---|---|
| The statement is not the headline | 20 | The checked statement is a different object, a weaker or partial statement, has a moved clause, an old or degenerate target, or is missing, so the proof can pass while the headline stays unchecked. |
| One kernel, one party | 17 | The second kernel is mostly off, checks are run by the claimant or graded by AI, and the few rebuilds often vendor the claimant's construction modules. |
| Custom definitions are trusted | 14 | Machine models, encodings and definitions written in the challenge file, and Comparator definition holes compared by type only, are part of what a reader must trust. |
| Missing files and checkers that stop short | 14 | Matrices, certificate files, witnesses, execution archives and ancillary files are not published, or a shipped checker skips what it names. |
| Floats and tolerances in the checker | 8 | Numerical certificates were checked with floating-point verifiers, tolerances, sampling grids or one-sided validators. |
| Large computations nobody has replayed | 8 | The cost of replaying a search or a build (pod-hours, memory, unreleased tooling) is itself the open gap. |
| Existence without a witness | 5 | Objects are proved to exist and never shown, or a disproof is non-effective. |
| Gaps the claimant declares | 5 | Some claimants list their own gaps by design, and those declared gaps become the audit's reading list. |
| Credit and novelty, not correctness | 5 | Literature rediscovery, priority disputes and withdrawals bear on credit rather than on whether a checked statement holds. |
In October 2026 OpenAI and Anthropic each published a Lean proof that the Exponential Time Hypothesis is false. Both proofs check. Each is stated for a machine and an input format of its own lab's choosing, so the question left is whether those statements are the textbook ETH. This is where that question stands, step by step, as of 2026-11-04.
The page on the two proofs is /eth/; the plan for the open steps is pre-registered in notes/eth-model-gap-preregistration-2026-11-04.md.
| claim | formal | checked by others | decided here | still open |
|---|---|---|---|---|
| Bulk release of 719 machine manuscripts in about 373 families; about 185 main results have Lean, checked by 405 to 416 Comparator challenges 2026-10-06 · sources 1 2 | Lean | Commelin (remarks in Quanta, not a check) | CERTIFIED 398 of 416 Comparator challenges accepted by two kernels (Lean and nanoda) at fd4aeeb2; 18 REFUSED for resources; none rejected certs/openai-math-kernel.json#/counts/words · report | Five headlines rest on no checked statement; 34 of 242 formalized families state less than they claim; 63 of 65 definition holes are compared by type only; nanoda on for 2 of 416; 15 witnesses unpublished |
| A sign error withdraws the Weil-classes paper on split abelian eightfolds and two dependent papers; 14 papers revised 2026-10-07 · sources 1 | none | finder not named | not examined here | Only unformalized results were affected; the README's warning that unformalized results could have issues applies |
| 3D Navier-Stokes blow-up with a smooth force (Clay alternatives C and D), plus unforced Euler blow-up; 166 pages and about 600k lines of Lean 2026-09-08 · sources 1 2 | Lean | Clay Mathematics Institute (evaluating, no decision); Bastounis, Circelli, Hansen | CERTIFIED Built here; Comparator and nanoda on both configurations; standard axioms only; at f9e8bc5b the Lean proves Theorem 1.1 as stated, finite energy included (PARTIAL at the announced 8937a8f4) certs/claims-ledger.json#/rows/54 · report | The force is inside the statement; 13 places where the paper asserts without showing; the analytic core was read, not decided |
| ETH is false: deterministic exact #k-CNF counting in subexponential time and polynomial space (family 378, SubexponentialSAT) 2026-10-26 · sources 1 2 | Lean | Impagliazzo-Paturi-Williams working group (letter says not certification; no outcome yet); Fortnow (comment, not a verification); O'Donnell, Kintali, Sellke (expositions) | CERTIFIED Comparator with Lean's kernel, nanoda and leanchecker --fresh at 7ef5c0cc; a Lean bridge proves the claim refutes textbook ETH in OpenAI's own machine model certs/eth-kernel.json#/rows/0 · page | The machine model (PrimitiveMachine) and CNF encoding are custom and defined in the challenge file; the step across machine models is prose; the release config ships with nanoda off |
| Local smoothing in all dimensions n >= 2, with Bochner-Riesz, Kakeya maximal and dimension, Stein square function and spherical restriction consequences 2026-10-26 · sources 1 · confidence P | Lean | — | CERTIFIED Kernel lane only (one of 18 of 20 at 7ef5c0cc); no statement reading run certs/openai-math-kernel-7ef5c0cc.json#/rows/11 · report | Custom definitions in the trusted base (halfWaveIntegral, IsKakeyaSet, kakeyaMaximal, literalSteinSquareFunction) not read against the literature |
| Rational Hodge conjecture for CM abelian varieties in every dimension 2026-10-06 · sources 1 2 | Lean | an outside replayer (not named until they consent) found the statement mismatch | READ Statement read at 7ef5c0cc: challenge and solution name different constants, so Comparator's statement comparison cannot pass; kernel REFUSED for resources certs/openai-math-hodge-statement.json#/word · report | The statement imports HodgeConjecture.Variants and OAI definitions that must be trusted; repaired upstream 10-29 (PR #4), not re-run here |
| Quasi-Riemann hypothesis: no zeros of zeta or Dirichlet L-functions for Re s > 7/8; Hecke variant 2026-09-30 · sources 1 · confidence P | Lean | Sarnak (not a theorem until humans check it); Tao (still being digested, 10-19) | CERTIFIED Kernel lane at fd4aeeb2; lane S reads the statement as riemannZeta s != 0 on Mathlib's zeta (family 003 MATCHES) certs/openai-math-kernel.json#/rows/286 · report | One kernel upstream; the human-edited 11/12 write-up is not formal |
| Uniform exclusion of Landau-Siegel zeros 2026-10-01 · sources 1 · confidence P | Lean | Tao (sketch of Green's reformulation, an exposition) | CERTIFIED Kernel lane only (challenge SiegelZeros, at fd4aeeb2) certs/openai-math-kernel.json#/rows/318 · report | Statement not compared with the headline here |
| Hadwiger's conjecture is false for graphs with independence number at most 2 2026-09-23 · sources 1 2 · confidence P | Lean | E. Bonnet (kernel replay that vendors OpenAI's 288 construction modules) | CERTIFIED Kernel lane only (challenge HadwigerCounterexample, at fd4aeeb2) certs/openai-math-kernel.json#/rows/159 · report | hadwigerNumber and connectedMatchingNumber are defined in the challenge file; no second, independent construction |
| The plane is not 5-colourable (EuclideanFiveColor, family 158) 2026-10-06 · sources 1 | Lean | — | CERTIFIED Kernel lane; the displayed definition checked by a transfer check (TRANSFERS); the finite graph NEEDS DATA certs/openai-math-kernel.json#/rows/117 · report | The finite unit-distance graph exists by compactness and is never shown |
| Sidorenko's conjecture is false (family 161; H has 22 triples on 13 points) 2026-10-06 · sources 1 | Lean | rohanarun (exact certificates for parts, no new counterexample) | CERTIFIED Kernel lane; the host NEEDS DATA; a pilot found no explicit host up to N = 32 (7.9 GPU-hours, every margin positive) certs/openai-math-kernel.json#/rows/317 · report | The host lives on D x D matrices over F_q with D in the hundreds, then a sampled graph; no explicit counterexample exists |
| N(6) = 3: at most 3 mutually unbiased bases in dimension 6 (family 266) 2026-10-06 · sources 1 | other | maximusrufus (re-ran the search, 12.4 h on 16 threads) | CERTIFIED Consistency and coverage of the saved records only (19 of 19 checks); N(6) = 3 not decided certs/openai-math-mub6-records.json#/word · report | The execution archive the manuscript cites is not shipped; a full C++ replay on Linux is not done |
| Borsuk counterexample in dimension 9 2026-10-06 · sources 1 | Lean | — | CERTIFIED C_28a <= 9 decided from the earlier kernel record of BorsukNine (two kernels; statement MATCHES); nothing new computed; CERTIFIED given a reading of the statement certs/optq-ledger.json#/rows/8 · report | None at the finite layer |
| Other release headlines: Unique Games, omega <= 9/4, Hilbert's tenth over Q, Erdős-Turán AP, Kakeya 3D/4D, Erdős-Gallai 2026-09-23 · sources 1 · confidence U | Lean | — | not examined here | Only through the release-wide kernel lane and lane S; the per-headline statement gap is not established; Hilbert 10 over Q reportedly has no Lean |
| Existence of interacting 4D QFT, including Yang-Mills and QCD; Lean said to be finished 10-16 2026-10-26 · sources · confidence U | none | a physics group (Gross, Douglas, Jaffe, Klebanov, Nekrasov) writing it up | not examined here | Nothing public to check |
| GPT-6 Astra disproves Erdős #1 (sum-distinct sets) in Lean 2026-08-28 · sources 1 2 | Lean | Bloom (exposition) | CERTIFIED Made effective: explicit sum-distinct sets below Bohman, 34 of 41 verified instances, smallest n = 1,701 certs/erdos1-ledger.json#/counts · report | The original disproof is non-effective (Smith-form limit); the buffer law K = O(d) is measured, not proved |
| IMO 2026 perfect or gold score by an OpenAI model 2026-07 · sources 1 · confidence U | none | — | not examined here | No official claim found; secondary reports only |
| claim | formal | checked by others | decided here | still open |
|---|---|---|---|---|
| More than 2/3 of zeta zeros are simple and on the critical line, and at least 5/6 are distinct; proof found by Claude 2026-08-10 · sources 1 2 3 | Lean | Lamzouri (independent new proof); mdumitrean (improved to 0.6728005676, kernel-checked) | CERTIFIED The numerical certificate re-checked without Lean, as concordance, not as verification of the ceiling; window constants raised to 0.86864150 / 0.93432075 corpus/claimbox-riemann/records/riemann-run.json · page | The side ceiling p0 <= 0.6818287 takes EnclOK as a hypothesis; its certificate file cert_N256_blk_b128m.json is unpublished |
| ETH is false: #3-SAT in subexponential time on Mathlib Turing machines (MainResults.ETHIsFalse) 2026-10-26 · sources 1 2 | Lean | Impagliazzo-Paturi-Williams working group; TSavo (bridge) | CERTIFIED Comparator with Lean's kernel, nanoda and leanchecker --fresh; the bridge proves #ETH and not-ETH in the claim's own model certs/eth-kernel.json#/rows/1 · page | The README says no machine checks that the file says what the paper says; the main theorem needs m >= 2, n >= 4 and every variable to occur; TM steps to RAM time is informal |
| Third-party bridges between the two ETH claims: TSavo (OpenAI's claim implies Anthropic's statement) and Hawkley (OpenAI's model to Anthropic's ETHIsFalse inside OpenAI's environment) 2026-10-29 · sources 1 | Lean | the bridge authors themselves | CERTIFIED Both bridges replayed; the version seam measured DIFFERENT (real-number arithmetic differs between the two Mathlibs) certs/eth-tsavo-bridge.json#/word · page | No single kernel has compared the two labs' statements across the Lean/Mathlib version seam |
| Hadamard matrices of order 668 and the other open orders below 2000, by three humans and Claude 2026-08-12 · sources 1 2 · confidence P | none | VibeMathed (reportedly decoded and checked H Ht = nI); Epoch (provisionally solved) | NEEDS DATA Search target DEAD; no matrix file found, so no check corpus/targets.json | No dataset or technical report is published; the check is one line once the bytes exist |
| Forced 3D Euler blow-up (Buckmaster and Alpöge; Lean written by Claude) 2026-08-15 · sources 1 · confidence P | Lean | — | not examined here | The result is forced Euler, not Navier-Stokes; not replayed |
| Lean formalization of Alman and Vassilevska Williams: 3SUM in O(n^1.9992) and APSP in O(n^2.99942) 2026-10-06 · sources 1 · confidence P | Lean | — | not examined here | The word-RAM is a 139-line custom file; the README lists running times not proved for any machine |
| FlashProve: zero-knowledge proofs of inference for Llama 4 Maverick, soundness proved in Lean 2026-10-30 · sources 1 | Lean | — | OPEN In progress, pre-registered 2026-11-04 (notes/flashprove-preregistration-2026-11-04.md): routes 1–2 on a hosted runner, the Lean library on a CPU pod; no verdict yet corpus/targets.json#/targets/133/verdict | Proved only for the Lean verifier in the random-oracle model; the C++ verifier and CUDA prover are tested, not proved; the served float model is not the one proved; zero knowledge proved for one request |
| claim | formal | checked by others | decided here | still open |
|---|---|---|---|---|
| AlphaProof Nexus: 9 of 353 Erdős problems and 44 of 492 OEIS conjectures, in Lean 2026-05-21 · sources 1 2 | Lean | lazarus-boop (rebuilt, audited axioms); rwst (re-adding results to OEIS) | CERTIFIED All 9 Erdős proofs plus the corrected #741(i): Comparator against formal-conjectures plus nanoda certs/apn-kernel.json#/counts · report | The 9 statements cover 7 problem numbers; #741(i) published in a demoted reading; 38 of 44 OEIS proofs published; 3 targets already proved; 2 statements degenerate |
| Cryptids: small Turing machines whose halting is equivalent to not-Goldbach (21 states), not-Con(ZF) (380) or not-RH (95); BB(6) and BB(3,3) holdouts 2026-10-09 · sources 1 2 3 | Lean | community PRs (winger, RH 95); Wieser (review acknowledged) | CERTIFIED Audited twice: 152 claims, 143 CERTIFIED, 1 REFUTED, 8 REFUSED; kernel lane CERTIFIED (Lean and nanoda) certs/cryptids-audit.json#/summary · report | ZF write-up transition counts off by one; riemann_104 checkpoint k undefined; verify.py checks theorems by substring and skips a stage it names; BB(6) labels subject to community acceptance |
| AlphaEvolve Ramsey lower bounds: 18 graphs, for example R(4,21) >= 244 and R(8,18) >= 1052 2026-10-22 · sources 1 2 | none | maximusrufus (partial re-run; did not finish R(10,12) or R(7,13)) | CERTIFIED 17 of 18 by an exact clique search (R(7,13): 613e9 nodes); R(8,18) REFUSED, about 60 pod-hours, parked certs/ramsey-ledger.json#/counts · report | The notebook ships unexecuted and reads only the upper triangle; R(8,18) >= 1052 has no independent check anywhere |
| AlphaEvolve problem repository: 67 problems, 19 records, with community certificates in issues #4 to #12 2026-06 · sources 1 2 3 | none | maximusrufus (verifier bugs: t-design check always true, difference-basis miscount, NaN/inf accepted) | CERTIFIED Community certificates: 70 CERTIFIED, 2 REFUSED certs/aerp-ledger.json#/counts · report | Records are often published as a program, not an object; the verifiers compare floats |
| AlphaEvolve-assisted bound omega < 2.371177, with Alman, Vassilevska Williams et al. 2026-08 · sources 1 2 · confidence P | none | — | not examined here | verification.py uses floats and is for search; the rigorous check is a separate rational Colab; no Lean |
| AlphaEvolve K(11) >= 593 and the rank-48 4x4 matrix-multiplication scheme over C (2025, the baseline) 2025-05 · sources | none | many | CERTIFIED K(11) >= 593 in the kissing ledger, exact; the rank-48 scheme exactly over Z[i] certs/kissing-ledger.json#/rows/2 · report | Included only as the baseline that June to November claims improved on |
| Gemini Deep Think at IMO 2026 2026-07 · sources · confidence U | none | — | not examined here | No official 2026 DeepMind claim found |
| claim | formal | checked by others | decided here | still open |
|---|---|---|---|---|
| Axiom Complete Lean proof of the classification of finite simple groups (43.1M lines, 2.05M declarations, 24 days) 2026-10-26 · sources 1 2 | Lean | Kim Morrison (lint PRs, no verdict); lean-eval (limit raised to 10 GB, no scored result) | ON HOLD Scouted, OPEN, held on the operator's word; not buildable on a laptop or a hosted runner corpus/targets.json#/targets/126/verdict | The statement is TauCeti's ClassificationStatement and nothing proves its list of groups is the textbook list; about 8 GB of certificate data; no oleans published; sorry-free is Axiom's word alone |
| Axiom Every finite simple group is 2-generated, from the CFSG development 2026-11-02 · sources 1 · confidence P | Lean | — | not examined here | Inherits every gap of the CFSG claim |
| Axiom AxiomProver 42/42 at IMO 2026, with Lean 2026-07-16 · sources 1 · confidence P | Lean | — | not examined here | AxiomProver wrote the formal problem statements itself, with no human audit found; checked through Axiom's own service plus a local Comparator run |
| Axiom With Cureton and Thorner: uniform zero-free region for Dedekind zeta (Re s > 31/32), building on OpenAI's quasi-RH 2026-10 · sources 1 · confidence P | Lean | Frei, Sofos, Widmer (state they have not verified it) | not examined here | Depends on vendored class-field-theory code; the constant changed between versions |
| Axiom zeta(5) is irrational: Fauzan's human proof, with AI Lean formalizations by Axiom and others 2026-09-17 · sources 1 2 · confidence P | Lean | several mutually independent Lean developments reaching the same formal-conjectures statement | not examined here | The mathematics is human; Axiom's version runs on a sorry-free PNT fork; not peer-reviewed |
| Lech Mazur / ProofAtlas A positive density of n reach 1 within 10.46 ln n Collatz steps (Codex/GPT) 2026-09-05 · sources 1 · confidence P | Lean | — | not examined here | Not Collatz itself; no LeanChecker replay, no independent replay or paper review |
| Harmonic Aristotle with van Doorn et al.: 8 Kourovka Notebook group-theory problems 2026-07-20 · sources 1 · confidence P | Lean | human co-authors; shared with the Notebook's editors | not examined here | 21.149 is solved only in its old v43 wording; axioms are not listed |
| Plasma AI Lean proof of Erdős #809 for all k >= 3 2026-10-08 · sources 1 · confidence P | Lean | — | not examined here | Statements checked by AI sessions and an automated review only; no outside review |
| Together AI / EinsteinArena K(11) >= 604, plus about 11 leaderboard records over AlphaEvolve 2026-06-09 · sources 1 | none | The Station (independent exact 604-point configurations) | CERTIFIED The 604 decided exactly and congruent to the Station's (a signed permutation); SOTA table: 20 constructions, 16 exact, 4 REPAIRED certs/kissing-ledger.json#/rows/9 · report | The verifier was floating-point at first and the first submission overlapped; Monte-Carlo rows REFUSED; four README rows have no files |
| The Station (dualverse-ai) New results on 5 of 12 AlphaEvolve problems, including an exact 604 and finite-field Kakeya sets 2026-08-24 · sources 1 2 | Lean | overlap with EinsteinArena only | CERTIFIED The 604 configurations exact and congruent to EinsteinArena's; the 3-D Keller map CERTIFIED (det -6, non-injective); the rest of the pool OPEN certs/kissing-ledger.json#/rows/4 · report | The abstract does not say which results are Lean-checked and which are only exact constructions |
| Oxelra Qiushi Engine: kissing lower bounds in 19 dimensions (25, 27, 32 to 39, 43, 45, 49 to 55) 2026-09-22 · sources 1 | none | none other than cert-machine (credited in their README) | WITNESSED All 19 configurations checked pair by pair; the K(18) and K(25-31) wave: 11 decided, 0 violations, 2 REPAIRED certs/kissing-wave.json#/rows/2 · report | No other third party has checked them; Kravatsky's 49 to 96 publish counts only (NEEDS DATA) |
| Oxelra Disproof of Bandeira's Open Problem 0.2(a), the matrix AM-GM inequality in spectral norm 2026-06-16 · sources 1 | Lean | only cert-machine (issue #1, unanswered) | CERTIFIED Core decided on cert-machine's own certificate: the Lai-Lim (5,5) SOS SDP is infeasible at lambda = 120; the claimant's certificate decides only the SDP without the transpose certs/bandeira-ledger.json#/rows/0 · report | Their Lean assumes the pairing as a structure field and defines no SDP; PSD is shown by SymPy outside Lean |
| Oxelra Structural tensor-rank lower bound 21 for 3x3 matrix multiplication over F2, with Lean 2026-09-17 · sources 1 · confidence U | Lean | — | not examined here | UNSCOUTED here (corpus/targets.json /targets/127); what structural restricts is unread |
| HorizonMath Benchmark paper credits six discoveries to GPT-5.4 Pro and GPT-5.6 Sol Max 2026-09-10 · sources 1 | none | domain experts (per the paper) | REFUTED The diagonal-Ramsey certificate: its pair at lambda = 1 lies outside GNNW's region R, 56 of 201 points outside; Kakeya area CERTIFIED (6008623/55050240); the GPT-5.6 closed forms NEEDS DATA; the spinor form not decided certs/horizonmath-ledger.json#/rows/0 · report | The validator tests one orientation where the theorem needs both; the paper details three of the six discoveries |
| Gupta-Ndiaye-Norin-Wei G_AI from ChatGPT 5.6 Sol gives R(k,k) <= 3.78233^(k+o(k)), printed as preliminary and unverified 2026-08-29 · sources 1 | none | none (the authors call it unverified) | CERTIFIED Theorem 14 holds on all of (0, 1] by two programs; further rounds reach 3.77213 certs/gnnw-certificate.json#/decided/verdict · report | Lower published records (3.769 with Lean by the authors; 3.69507) are not checked here |
| Gao Keller / Jacobian counterexamples (Claude assisting) and Markus-Yamabe fields first published in a ChatGPT gist 2026-08 · sources 1 2 | none | pith.science review (flags wording) | CERTIFIED 7 CERTIFIED, 1 PARTIAL (F7's determinant rests on the paper's lemma) certs/polymaps-ledger.json#/byVerdict · report | The promised ancillary files are not on arXiv; the 18-dimensional unipotency is checked in the paper at one sample point |
| AI-assisted authors (six manuscripts) Six AI-assisted manuscripts: Maxwell point charges, Korenblum c2 >= 0.4263, Erdős #1038, Ran-Teng Conjecture 20, Mathieu property, rank-two Poisson 2026-02 · sources 1 | none | the authors' own float or Arb checks | CERTIFIED 5 CONFIRMED, 1 PARTIAL (the record's words); in each, the computational fragment only certs/ai-claims-summary.json#/verdicts · report | In 6 of 6 the analytic core is prose; Maxwell holds at epsilon = 1/6 only; source checks were floating-point with no artefact |
| Jason Davies GPT-6 Astra: exactly ten minimum universal sets of 12 MacMahon cubes (Johnson-Roldán Conjectures 4 and 8) 2026-11-01 · sources 1 | Lean | Vilin97 (LeanPool PR #730 rebuild); Palomar registry (automated) | CERTIFIED Decided twice: 300 of 300 witnesses rebuilt with independent geometry; Comparator and nanoda; statement reading MATCHES certs/macmahon-kernel.json#/verdict · report | Necessity rests on Lean, not on a second exact search; the numerical histograms are outside Lean |
| MIT CSAIL Weight-Space Programming: GPT-6 Astra edits Qwen3.5-0.8B weights; MATH-500 from 7.9% to 48.1% 2026-11-02 · sources 1 | none | KidIkaros (reproduced the edit); Honnibal, Goedecke (critiques) | CERTIFIED The edit: 2 tensors, 130,188 entries; the gain is termination, mostly a settings effect; 'tuned on the test set' REFUTED; 'PPO weak' REFUSED certs/wsp-weights.json#/verdicts · report | An ML claim adjacent to mathematics; the authors' issue window closed 11-04 |
| Epoch AI FrontierMath Open Problems: 10 of about 50 solved (5 by AI alone, 5 human plus AI), including Hadamard 668 2026-03 · sources 1 · confidence P | other | Epoch's verifiers and the problem authors | OPEN 18 AI-autoformalized Erdős statements scouted, no fidelity defect on a first reading; the census adds that the Chowla verifier was fooled by a demo set corpus/targets.json#/targets/60/verdict | Labels conflict with the changelog for 2 entries; sampling-based verifiers can be gamed |
| Erdős problems community AI contributions to Erdős problems (teorth wiki): about 69 full-solution rows; 25 rows where the literature was found afterwards 2026-06-30 · sources 1 · confidence P | Lean | Bloom, Tao and editors (classify rows) | NEEDS DATA Pool DEAD as witness claims (proofs, not objects); #513 registered as expected NEEDS DATA, not decided corpus/targets.json | Rediscovery is common (19 of 25 similar); statement fidelity unaudited; post-June AI claims not on the wiki |
| several Third-party Lean claims seen on X: Murty-Simon (Erdős #742), a Global Attractor case, Euclid uniform processes, distinct distances, a Diophantine equation equivalent to Con(ZFC) 2026-10-24 · sources 1 · confidence P | Lean | — | OPEN All scouted 11-03; none built corpus/targets.json#/targets/138/verdict | Each needs a statement reading and a two-kernel replay; for Con(ZFC) the authors mark separate finite checks as open |
| several IMO 2026 by others: Huawei / Xiaohongshu 42/42, NVIDIA Nemotron 30/42, Kimi K3, DeepSeek and Grok via deedy/imo-2026 2026-07 · sources 1 · confidence U | none | IMO organisers' grading as reported (AFP via France24) | not examined here | No IMO statement or transcripts found; one harness grades with AI and showed a model the reviewer's findings before repairs |
| Zhi-Wei Sun Catalan's constant is irrational (AI-produced numerical data) 2026-09-03 · sources 1 · confidence U | none | Wachs (finds the main estimate unjustified) | not examined here | Disputed; a reported parallel OpenAI claim could not be confirmed |
| CSLib complexitylib (AI agents) Native re-proof that ETH and SETH are false on a standard deterministic multitape Turing machine with a binary encoding, and that word RAMs simulate multitape machines in linear time 2026-10-27 · sources 1 2 3 | Lean | an AI reviewer outside both authoring contexts (per the PR) | CERTIFIED Built at 1b7d62a8; the headlines rest on the three standard axioms (our file); nanoda accepts not_eth, exact_count and executes_simProgram; leanchecker --fresh replays the abstract module certs/eth-cslib-d1.json#/verdict | Proposition 6.4's bound, not Theorem 1.1's; a re-proof, not a bridge from either lab's statement; ETH on a word RAM at logarithmic word size is not covered (the RAM inclusions need polynomial time) |