{"version":1,"generated":"2026-10-01","license":"CC BY 4.0","fields":["id","title","claim","field","date","added","lab","model","verification","autonomy","tags","humans","year_posed","sources","registrations","url"],"total":142,"count":142,"offset":0,"entries":[{"id":"2026-09-26-erdos-1220-not-provable","title":"Erdős Problem #1220 formalized as not provable in ZFC, from a 1987 Shelah-Stanley consistency result","claim":"A Lean 4 formalization shows that ZFC cannot prove a positive answer to Erdős Problem #1220 on partition relations for singular cardinals, by formalizing Shelah and Stanley's 1987 forcing construction, with AI models assisting on the Lean code.","field":"mathematics","date":"2026-09-26","added":"2026-09-28","lab":"Independent","model":"Claude Opus 5.5 (Claude Code); Astra (OpenAI Codex)","verification":"author-verified","autonomy":"ai-assisted","tags":["set-theory","erdos","lean","formalization","forcing"],"humans":["Ji Ho Bae"],"year_posed":1971,"sources":[{"label":"GitHub: jbaelaw/erdos1220-lean","url":"https://github.com/jbaelaw/erdos1220-lean","kind":"research"},{"label":"Erdős Problems: problem #1220","url":"https://www.erdosproblems.com/1220","kind":"commentary"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-09-26-000001","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-09-26-000001&version=1","repository":"jbaelaw/erdos1220-lean","commit":"9cb81ffa48ffb766127c7e485ccef77bd4160868","theorems":["erdos1220_not_provable","erdos1220_sentence_faithful"],"checked":"2026-09-26"}],"url":"https://whataifound.org/finding/2026-09-26-erdos-1220-not-provable"},{"id":"2026-09-26-lovasz-cayley-polylog-degree","title":"Hamilton cycles in connected Cayley graphs of polylogarithmic degree, toward the Lovász conjecture","claim":"Every connected Cayley graph on \\(n\\) vertices with degree at least \\(C(\\log n)^{13}/\\log\\log n\\) has a Hamilton cycle, lowering the degree threshold in the Cayley-graph form of the Lovász conjecture from a power of \\(n\\) to a power of \\(\\log n\\); the manuscript was drafted by GPT 6 Pro and the proof formalized in Lean by Claude agents.","field":"mathematics","date":"2026-09-26","added":"2026-09-28","lab":"Independent","model":"GPT 6 Pro (manuscript draft); Claude Opus 5.5 agents in Grok Build (Lean formalization)","verification":"claimed","autonomy":"collaborative","tags":["graph-theory","combinatorics","lovasz-conjecture","lean","formalization","argument"],"humans":["Domagoj Bradač","Matija Bucić","Micha Christoph","Zach Hunter","Oliver Janzer","Alp Müyesser","Shengtong Zhang"],"year_posed":1969,"sources":[{"label":"GitHub: ShengtongZhang-alt/lovasz-opus, the draft and its Lean formalization","url":"https://github.com/ShengtongZhang-alt/lovasz-opus","kind":"research"},{"label":"Bedert, Draganić, Müyesser and Pavez-Signé: the prior n¹⁻ᶜ threshold","url":"https://arxiv.org/abs/2603.08675","kind":"research"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-09-26-000003","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-09-26-000003&version=1","repository":"ShengtongZhang-alt/lovasz-opus","commit":"ee0085ddec79996279c7b52044659032e5cf8431","theorems":["Lovasz.hamiltonian_of_polylog_degree"],"checked":"2026-09-26"}],"url":"https://whataifound.org/finding/2026-09-26-lovasz-cayley-polylog-degree"},{"id":"2026-09-25-nine-loop-hexagon-amplitude","title":"Six-particle MHV amplitude in planar N=4 super Yang-Mills computed at nine loops","claim":"Claude computed the six-particle maximally-helicity-violating amplitude in planar \\(\\mathcal{N} = 4\\) super Yang-Mills theory at nine loops, one loop beyond the previous record, from a single prompt naming the problem.","field":"physics","date":"2026-09-25","added":"2026-10-01","lab":"Anthropic","model":"Claude Fable 5.1 (in Claude Science)","verification":"author-verified","autonomy":"ai-led","tags":["scattering-amplitudes","quantum-field-theory","agents","computation"],"humans":["Liam Fitzpatrick","Siddharth Mishra-Sharma"],"sources":[{"label":"Anthropic: Yes, Claude can do nine loops","url":"https://www.anthropic.com/research/yes-claude-can-do-nine-loops","kind":"announcement"},{"label":"Zenodo: nine-loop six-gluon MHV amplitude, large data files","url":"https://zenodo.org/records/22949278","kind":"research"},{"label":"Cosmic9: symbol and function files with validation records","url":"https://smsharma.io/cosmic-nine-loops/","kind":"research"}],"url":"https://whataifound.org/finding/2026-09-25-nine-loop-hexagon-amplitude"},{"id":"2026-09-23-array-associated-reverse-transcriptases","title":"Agent-run genome survey identifies array-associated reverse transcriptases in jumbo phages","claim":"Claude agents surveying reverse transcriptase genes across 1.9 billion metagenomic protein clusters flagged a family of jumbo-phage reverse transcriptases paired with an array of repeated non-coding DNA units and a dedicated partner gene, an arrangement the authors say fits no described reverse transcriptase class.","field":"biology","date":"2026-09-23","added":"2026-09-24","lab":"Anthropic","model":"Claude Mythos 5","verification":"claimed","autonomy":"collaborative","tags":["genomics","bacteriophage","multi-agent","autonomous-discovery"],"humans":["Peter H. Yoon","Januka S. Athukoralage","Emmanuel Ameisen","Eric Kauderer-Abrams","Nicholas T. Perry","Matthew G. Durrant"],"sources":[{"label":"Anthropic preprint: Autonomous AI agents discover reverse transcriptases with tandem repeat arrays","url":"https://www-cdn.anthropic.com/22573675ada52a8ca8a97a1a4b4326b2f208a071.pdf","kind":"research"},{"label":"Korn et al. 2021, the MarsHill genome report that first identified the reverse transcriptase","url":"https://doi.org/10.1128/jvi.02391-20","kind":"research"},{"label":"Anthropic: Claude discovers a novel enzyme system with CRISPR-like repeats","url":"https://www.anthropic.com/news/claude-discovers-novel-enzyme-system","kind":"announcement"}],"url":"https://whataifound.org/finding/2026-09-23-array-associated-reverse-transcriptases"},{"id":"2026-09-17-rogers-ramanujan-torus-knot","title":"Huang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputs","claim":"The geometric extension of the Rogers-Ramanujan and Andrews-Gordon identities conjectured by Huang, Jiang and Oblomkov is proved for every torus-knot singularity with coprime exponents, via a stronger finite identity.","field":"mathematics","date":"2026-09-17","added":"2026-09-22","lab":"Axiom Math","model":"AxiomProver","verification":"claimed","autonomy":"ai-assisted","tags":["number-theory","combinatorics","q-series","lean","formalization","argument"],"humans":["Yifeng Huang","Kenny Lau","Ken Ono"],"sources":[{"label":"arXiv: Rogers-Ramanujan identities from the geometry of Xᵃ = Yᵇ","url":"https://arxiv.org/abs/2609.20567","kind":"research"},{"label":"GitHub: AxiomMath/HJO, the Lean formalization","url":"https://github.com/AxiomMath/HJO","kind":"research"}],"url":"https://whataifound.org/finding/2026-09-17-rogers-ramanujan-torus-knot"},{"id":"2026-09-17-talagrand-operator-cotype","title":"Counterexample to Talagrand's operator cotype problem","claim":"An operator is exhibited whose Rademacher cotype is not controlled by the maximum of its Gaussian cotype and its (q,1)-summing norm, answering Talagrand's question in the negative already at q equals 2.","field":"mathematics","date":"2026-09-17","added":"2026-09-22","lab":"Independent","model":"ChatGPT (GPT-5.6)","verification":"claimed","autonomy":"ai-led","tags":["functional-analysis","probability","counterexample","construction"],"humans":["Xinglong Wu"],"sources":[{"label":"arXiv: A Counterexample to Talagrand’s Operator Cotype Problem","url":"https://arxiv.org/abs/2609.19731","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"talagrand-operator-cotype-problem","url":"https://vibemathed.com/problem/talagrand-operator-cotype-problem"}],"url":"https://whataifound.org/finding/2026-09-17-talagrand-operator-cotype"},{"id":"2026-09-16-browning-sawin-hypersurfaces","title":"Browning-Sawin conjecture on random sign-coefficient hypersurfaces proved, with a Lean formalization assuming existing literature","claim":"Random hypersurfaces with coefficients drawn uniformly from plus and minus one are shown to be smooth with probability tending to one as the degree grows, with a quantitative rate.","field":"mathematics","date":"2026-09-16","added":"2026-09-22","lab":"Axiom Math","model":"AxiomProver","verification":"claimed","autonomy":"ai-assisted","tags":["algebraic-geometry","probability","arithmetic-statistics","lean","formalization","argument"],"humans":["Ken Ono","Ashvin Swaminathan"],"year_posed":2025,"sources":[{"label":"arXiv: On a conjecture of Browning and Sawin on random hypersurfaces with sign coefficients","url":"https://arxiv.org/abs/2609.18879","kind":"research"},{"label":"GitHub: AxiomMath/BrowningSawin, the Lean formalization","url":"https://github.com/AxiomMath/BrowningSawin","kind":"research"},{"label":"arXiv: Browning and Sawin, Random Diophantine equations of large degree, the source of the conjecture","url":"https://arxiv.org/abs/2510.26191","kind":"research"}],"url":"https://whataifound.org/finding/2026-09-16-browning-sawin-hypersurfaces"},{"id":"2026-09-16-four-color-theorem-lean","title":"Four Color Theorem formalized in Lean 4 by AI agents, in two independent developments","claim":"Two independent Lean 4 proofs of the Four Color Theorem, each following Gonthier and Werner's Coq proof and each written almost entirely by a Claude model under one person's direction, resting only on Lean's three standard axioms.","field":"mathematics","date":"2026-09-16","added":"2026-09-28","lab":"Independent","model":"Claude Fable 5.1 and Claude Opus 5 (Emery); Claude Opus 5.5 (Barish)","verification":"claimed","autonomy":"ai-led","tags":["graph-theory","four-color-theorem","lean","formalization"],"humans":["Chris Emery","Robert D. Barish"],"year_posed":1852,"sources":[{"label":"GitHub: corun1024/4ct, Chris Emery's Lean 4 proof","url":"https://github.com/corun1024/4ct","kind":"research"},{"label":"GitHub: RBarish-UTokyo/FourColorTheorem-Lean4, Robert D. Barish's port","url":"https://github.com/RBarish-UTokyo/FourColorTheorem-Lean4","kind":"research"},{"label":"GitHub: math-comp/fourcolor, Gonthier and Werner's Coq proof that both follow","url":"https://github.com/math-comp/fourcolor","kind":"research"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-09-27-000005","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-09-27-000005&version=1","repository":"RBarish-UTokyo/FourColorTheorem-Lean4","commit":"20fa34599f5189dd569d96dd22f306c94ab1c446","theorems":["FourColor.RealPlane.four_color"],"checked":"2026-09-27","note":"Covers Barish's port only; Emery's development carries no registration."}],"url":"https://whataifound.org/finding/2026-09-16-four-color-theorem-lean"},{"id":"2026-09-15-bit-php-resolution-over-parities","title":"Exponential lower bound for the bit pigeonhole principle in unrestricted resolution over parities","claim":"Any refutation of the bit pigeonhole principle in resolution over parities, a proof system whose lines are disjunctions of linear equations mod 2, must be exponentially long even with no restriction on its depth or regularity; the mathematics was produced by AI models and the main theorem is checked in Lean.","field":"computer-science","date":"2026-09-15","added":"2026-09-28","lab":"Independent","model":"GPT-6 Astra (mathematics, version 1 formalization and drafting); Claude Fable 5.1 and Claude Opus 5 (revision 1 formalization)","verification":"claimed","autonomy":"ai-led","tags":["proof-complexity","pigeonhole-principle","lean","formalization","argument"],"humans":["Kamil Braun"],"sources":[{"label":"arXiv: An exponential lower bound for the bit pigeonhole principle in resolution over parities","url":"https://arxiv.org/abs/2609.23015","kind":"research"},{"label":"GitHub: kbr-/math-research, the preprint sources and Lean formalization","url":"https://github.com/kbr-/math-research","kind":"research"},{"label":"Byramji and Impagliazzo: the prior bounded-depth result","url":"https://arxiv.org/abs/2511.20023","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"superpolynomial-lower-bounds-for-bit-php-in-unrestricted-resolution-over-paritie","url":"https://vibemathed.com/problem/superpolynomial-lower-bounds-for-bit-php-in-unrestricted-resolution-over-paritie"}],"url":"https://whataifound.org/finding/2026-09-15-bit-php-resolution-over-parities"},{"id":"2026-09-15-ipm-forced-blowup","title":"Finite-time blowup for the IPM equation with uniformly space-time smooth forcing","claim":"The incompressible porous medium equation on the two-dimensional torus is shown to develop a finite-time singularity under a force that is smooth in space and time together, extending a result previously available only for spatially smooth forcing.","field":"mathematics","date":"2026-09-15","added":"2026-09-22","lab":"Independent","model":"Not named; the arXiv comment field states only that the proof is LLM-assisted","verification":"claimed","autonomy":"ai-assisted","tags":["pde","fluid-dynamics","singularity","argument"],"humans":["Levent Alpöge","Tristan Buckmaster","Matei P. Coiculescu"],"sources":[{"label":"arXiv: Extending the Cordoba-Martinez-Zoroa IPM Blow-Up to Uniformly Space-Time Smooth Forcing","url":"https://arxiv.org/abs/2609.16470","kind":"research"},{"label":"arXiv: Cordoba and Martinez-Zoroa, the prior spatially-smooth-forcing result","url":"https://arxiv.org/abs/2410.22920","kind":"research"},{"label":"Terence Tao on the forced-blowup results for IPM, Boussinesq and Euler","url":"https://terrytao.wordpress.com/2026/09/07/finite-time-blowup-with-smooth-forcing-term-for-the-incompressible-porous-medium-boussinesq-and-incompressible-euler-equations/","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"ipm-blowup-spacetime-smooth-forcing","url":"https://vibemathed.com/problem/ipm-blowup-spacetime-smooth-forcing","note":"The record credits Claude and Codex with GPT-5.6 Sol and labels the proof Lean-verified, linking tristanbuckmaster/fluid_lean. At commit d0124689230b58b4f86e7b90ac59de06404b3b6b that repository holds the companion Boussinesq and Euler developments and no IPM project, so neither claim is corroborated by an artifact."}],"url":"https://whataifound.org/finding/2026-09-15-ipm-forced-blowup"},{"id":"2026-09-14-nivat-conjecture","title":"Nivat's conjecture claimed in its sharp form, with the submitter stating he cannot check it","claim":"A Lean development claims Nivat's 1997 conjecture in full: if a two-dimensional configuration has at most mn distinct patterns on some m by n rectangle, it has a nonzero period.","field":"mathematics","date":"2026-09-14","added":"2026-09-15","lab":"Independent","model":"GPT-6 Pro (proof); GPT-6 Astra Ultra through Codex (Lean formalization)","verification":"claimed","autonomy":"ai-led","tags":["symbolic-dynamics","combinatorics","lean","formalization","argument"],"humans":["Boon Suan Ho"],"year_posed":1997,"sources":[{"label":"GitHub: boonsuan/nivat, the Lean 4 and mathlib formalization","url":"https://github.com/boonsuan/nivat","kind":"research"},{"label":"Palomar registration for the Nivat formalization","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-09-14-000003&version=1","kind":"research"},{"label":"Bryna Kra on AI and deep theorems, guest post on Terence Tao's blog","url":"https://terrytao.wordpress.com/2026/09/13/deep-theorems-were-scarce-and-difficult-and-so-became-an-effective-mechanism-to-identify-deep-thought-ai-has-broken-this-system/","kind":"commentary"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-09-14-000003","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-09-14-000003&version=1","repository":"boonsuan/nivat"}],"url":"https://whataifound.org/finding/2026-09-14-nivat-conjecture"},{"id":"2026-09-10-approval-committee-core","title":"Existence of the core in approval-based committee elections","claim":"Every approval-based multi-winner election is shown to admit a committee in the core, settling the main open question in the area, and one can be found in polynomial time.","field":"mathematics","date":"2026-09-10","added":"2026-09-22","lab":"Independent","model":"GPT-6 Astra","verification":"claimed","autonomy":"collaborative","tags":["social-choice","combinatorics","algorithms","argument"],"humans":["Patrick Becker","Matthias Greger","Dominik Peters"],"sources":[{"label":"arXiv: Existence of the Core in Approval-Based Committee Elections","url":"https://arxiv.org/abs/2609.11912","kind":"research"},{"label":"Epoch AI: FrontierMath open problems, committee election","url":"https://epoch.ai/frontiermath/open-problems/committee-election","kind":"announcement"}],"url":"https://whataifound.org/finding/2026-09-10-approval-committee-core"},{"id":"2026-09-09-small-undecidable-groups","title":"A 3-generator 9-relator group with unsolvable word problem, and smaller Adian-Rabin families","claim":"A group given by 3 generators and 9 relations has an unsolvable word problem, beating the 12-relation record Borisov set in 1969, and it yields families of 4-generator 11-relator and 2-generator 10-relator presentations for which no algorithm can decide whether the group is trivial.","field":"mathematics","date":"2026-09-09","added":"2026-09-24","lab":"Independent","model":"GPT-5.6 Sol Pro (construction); GPT-5.6 Sol in Codex (Lean formalization)","verification":"author-verified","autonomy":"ai-led","tags":["group-theory","logic","construction","lean","formalization"],"humans":["Marc Kegel","Shana Yunsheng Li","Qiuyu Ren"],"sources":[{"label":"arXiv: Small undecidable groups and unrecognizable 4-manifolds","url":"https://arxiv.org/abs/2609.10461","kind":"research"},{"label":"GitHub: 32805433/Adian-Rabin, the Lean 4 formalization of the algebraic results","url":"https://github.com/32805433/Adian-Rabin","kind":"research"},{"label":"arXiv: Tancer, Simpler algorithmically unrecognizable 4-manifolds, the prior deficiency-9 bound","url":"https://arxiv.org/abs/2310.07421","kind":"research"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-09-22-000002","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-09-22-000002&version=1","repository":"32805433/Adian-Rabin","commit":"fb4a401e8fbdba36e7b35c11fde2baa15592e185","theorems":["Undecidability.exists_three_generator_nine_relator_group_with_unsolvable_word_problem","Undecidability.exists_four_generator_eleven_relator_adian_rabin_family","Undecidability.exists_two_generator_ten_relator_adian_rabin_family"],"checked":"2026-09-22","note":"Registered by the paper's own authors. These are Theorems 1.1, 1.3 and 1.4; the record states that the four-manifold consequences are outside the formalized scope."}],"url":"https://whataifound.org/finding/2026-09-09-small-undecidable-groups"},{"id":"2026-09-08-euler-unforced-blowup","title":"Finite-time blowup for the unforced Euler equations from smooth compactly supported data","claim":"A Lean development proves that the three-dimensional incompressible Euler equations, with no forcing term, develop a singularity in finite time from smooth, compactly supported, divergence-free initial velocity on all of space.","field":"mathematics","date":"2026-09-08","added":"2026-09-10","lab":"OpenAI","model":"Unnamed OpenAI model described as more capable than GPT-6 Astra for the proof; GPT-6 Astra through Codex for the Lean formalization","verification":"claimed","autonomy":"ai-led","tags":["pde","fluid-dynamics","euler-equations","singularity","lean","formalization","argument"],"sources":[{"label":"GitHub: openai/NavierStokesAndEuler, the Lean 4 formalizations","url":"https://github.com/openai/NavierStokesAndEuler","kind":"research"},{"label":"OpenAI: Finite time blowup for the Euler equation (PDF)","url":"https://cdn.openai.com/pdf/315b36cd-ec98-4023-8342-93345194ece1/euler.pdf","kind":"research"},{"label":"OpenAI: On the Navier-Stokes Millennium Prize Problem, the announcement covering both results","url":"https://openai.com/index/navier-stokes-solution/","kind":"announcement"},{"label":"Chen and Hou: singularity formation in 3D Euler with smooth initial data and boundary, the closest prior result","url":"https://www.pnas.org/doi/10.1073/pnas.2500940122","kind":"commentary"},{"label":"Terence Tao on the Alpoge and Buckmaster forced-blowup results of the same week, a different claim","url":"https://terrytao.wordpress.com/2026/09/07/finite-time-blowup-with-smooth-forcing-term-for-the-incompressible-porous-medium-boussinesq-and-incompressible-euler-equations/","kind":"commentary"},{"label":"Science: How an AI math breakthrough ignited a controversy","url":"https://www.science.org/content/article/how-ai-math-breakthrough-ignited-controversy","kind":"coverage"}],"registrations":[{"registry":"vibemathed","id":"finite-time-blowup-for-the-3d-incompressible-euler-equations-unforced","url":"https://vibemathed.com/problem/finite-time-blowup-for-the-3d-incompressible-euler-equations-unforced"}],"url":"https://whataifound.org/finding/2026-09-08-euler-unforced-blowup"},{"id":"2026-09-08-navier-stokes-forced-blowup","title":"Finite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and D","claim":"A Lean development proves that three-dimensional Navier-Stokes with a smooth forcing term breaks down in finite time, at every positive viscosity, on both Euclidean space and the periodic torus, which is two of the four statements the Clay problem description asks for a proof of, though not the unforced regularity question the phrase usually brings to mind.","field":"mathematics","date":"2026-09-08","added":"2026-09-10","lab":"OpenAI","model":"Unnamed OpenAI model described as more capable than GPT-6 Astra for the proof; GPT-6 Astra through Codex for the Lean formalization","verification":"claimed","autonomy":"ai-led","tags":["pde","fluid-dynamics","navier-stokes","singularity","lean","formalization","argument"],"year_posed":2000,"sources":[{"label":"GitHub: openai/NavierStokesAndEuler, the Lean 4 formalizations","url":"https://github.com/openai/NavierStokesAndEuler","kind":"research"},{"label":"OpenAI: Finite time blowup for Navier-Stokes (PDF)","url":"https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf","kind":"research"},{"label":"Clay Mathematics Institute: the official problem description, alternatives (C) and (D) on page 2","url":"https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf","kind":"research"},{"label":"Formal Conjectures: the Lean statement of the Navier-Stokes problem the Comparator challenges adapt","url":"https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Millennium/NavierStokes.lean","kind":"research"},{"label":"OpenAI: On the Navier-Stokes Millennium Prize Problem","url":"https://openai.com/index/navier-stokes-solution/","kind":"announcement"},{"label":"Clay Mathematics Institute: statement on the Navier-Stokes announcement","url":"https://www.claymath.org/news/navier-stokes-announcement/","kind":"commentary"},{"label":"Terence Tao on the blowup results released the same week","url":"https://terrytao.wordpress.com/2026/09/07/finite-time-blowup-with-smooth-forcing-term-for-the-incompressible-porous-medium-boussinesq-and-incompressible-euler-equations/","kind":"commentary"},{"label":"vibemathed: finite-time breakdown with smooth forcing","url":"https://vibemathed.com/problem/navier-stokes-millennium-prize-problem-finite-time-breakdown-with-smooth-forcing","kind":"commentary"},{"label":"Quanta: AI has solved one of math's $1 million Millennium Prize problems","url":"https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-20260908/","kind":"coverage"},{"label":"Nature: OpenAI claims huge maths breakthrough on a famed Millennium Problem","url":"https://www.nature.com/articles/d41586-026-02842-5","kind":"coverage"},{"label":"Science: How an AI math breakthrough ignited a controversy","url":"https://www.science.org/content/article/how-ai-math-breakthrough-ignited-controversy","kind":"coverage"},{"label":"Buckmaster and Alpoge: public statement on the priority of the forced-blowup program (PDF)","url":"https://cims.nyu.edu/~tristanb/statement.pdf","kind":"challenge"},{"label":"Constantin, Ignatova and Vicol: the forcing in any construction with these features can be neither locally vanishing nor real-analytic in space","url":"https://arxiv.org/abs/2609.20803","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"navier-stokes-millennium-prize-problem-finite-time-breakdown-with-smooth-forcing","url":"https://vibemathed.com/problem/navier-stokes-millennium-prize-problem-finite-time-breakdown-with-smooth-forcing","note":"Recorded there as a candidate with review pending."}],"url":"https://whataifound.org/finding/2026-09-08-navier-stokes-forced-blowup"},{"id":"2026-09-07-complex-grothendieck-constant","title":"Improved lower bound for the complex Grothendieck constant","claim":"The complex Grothendieck constant is shown to exceed 1.35584631827168, closing more than a quarter of the gap between the long-standing Davie lower bound and the Haagerup upper bound.","field":"mathematics","date":"2026-09-07","added":"2026-09-22","lab":"Independent","model":"Odin Automatic AI Research Agent","verification":"author-verified","autonomy":"ai-led","tags":["functional-analysis","optimization","interval-arithmetic","construction"],"humans":["Shengtao Guo","Ethan X. Fang","Junwei Lu"],"sources":[{"label":"arXiv: An Improved Lower Bound for the Complex Grothendieck Constant","url":"https://arxiv.org/abs/2609.07000","kind":"research"},{"label":"GitHub: shengtaoguo/complex-grothendieck-certificates, the interval-arithmetic certificates","url":"https://github.com/shengtaoguo/complex-grothendieck-certificates","kind":"research"},{"label":"arXiv: Heilman, Jones and Malavolta, Sharper bounds for the complex Grothendieck constant","url":"https://arxiv.org/abs/2609.25462","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"lower-bound-for-the-complex-grothendieck-constant","url":"https://vibemathed.com/problem/lower-bound-for-the-complex-grothendieck-constant"}],"url":"https://whataifound.org/finding/2026-09-07-complex-grothendieck-constant"},{"id":"2026-09-06-bollobas-nikiforov","title":"Bollobas-Nikiforov conjecture claimed in full, in a weighted form","claim":"Five named mathematicians with AI assistance claim the 2007 Bollobas-Nikiforov conjecture for every noncomplete graph, bounding the sum of the squares of the two largest adjacency eigenvalues, with a Lean formalization.","field":"mathematics","date":"2026-09-06","added":"2026-09-15","lab":"Independent","model":"GPT-6 Astra (ideation and manuscript); Grok 4.6 (Lean formalization); Claude Fable 5.1 (submission packaging)","verification":"claimed","autonomy":"collaborative","tags":["graph-theory","spectral-graph-theory","combinatorics","lean","formalization","argument"],"humans":["Gabriel Coutinho","Yinchen Liu","Thomas Jung Spier","Quanyu Tang","Shengtong Zhang"],"year_posed":2007,"sources":[{"label":"GitHub: ShengtongZhang-alt/BN, the Lean 4 and Mathlib formalization","url":"https://github.com/ShengtongZhang-alt/BN","kind":"research"},{"label":"Giacomelli: the prior partial result, complete multipartite and dense K4-free graphs","url":"https://arxiv.org/abs/2603.26379","kind":"research"},{"label":"vibemathed: Bollobas-Nikiforov conjecture","url":"https://vibemathed.com/problem/bollobas-nikiforov-conjecture","kind":"commentary"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-09-07-000002","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000002&version=1","repository":"ShengtongZhang-alt/BN"},{"registry":"vibemathed","id":"bollobas-nikiforov-conjecture","url":"https://vibemathed.com/problem/bollobas-nikiforov-conjecture"}],"url":"https://whataifound.org/finding/2026-09-06-bollobas-nikiforov"},{"id":"2026-09-05-ibragimov-iosifescu","title":"Disproof of the Ibragimov-Iosifescu conjecture for phi-mixing sequences","claim":"A Lean development constructs a stationary phi-mixing sequence with finite second moments whose normalized partial sums fail to satisfy the central limit theorem, disproving a 1971 conjecture.","field":"mathematics","date":"2026-09-05","added":"2026-09-15","lab":"OpenAI / Epoch AI","model":"GPT-6 Astra (pre-release)","verification":"claimed","autonomy":"ai-led","tags":["probability","central-limit-theorem","lean","formalization","construction"],"humans":["Tom Adamczewski"],"year_posed":1971,"sources":[{"label":"GitHub: tadamcz/phi-mixing-clt, the Lean counterexample and literature review","url":"https://github.com/tadamcz/phi-mixing-clt","kind":"research"},{"label":"vibemathed: Ibragimov-Iosifescu phi-mixing CLT conjecture","url":"https://vibemathed.com/problem/ibragimov-iosifescu-varphi-mixing-clt-conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"ibragimov-iosifescu-varphi-mixing-clt-conjecture","url":"https://vibemathed.com/problem/ibragimov-iosifescu-varphi-mixing-clt-conjecture"}],"url":"https://whataifound.org/finding/2026-09-05-ibragimov-iosifescu"},{"id":"2026-09-04-fermat-last-theorem-lean","title":"Fermat's Last Theorem formalized end to end in Lean 4","claim":"A complete machine-checked proof of Fermat's Last Theorem in Lean 4, written by AI agents in eleven days, resting on Lean's three standard axioms and accepted by two independent kernels.","field":"mathematics","date":"2026-09-04","added":"2026-09-07","lab":"Anthropic","model":"Internal Anthropic research model, described in the announcement as roughly comparable to Claude Fable 5.1","verification":"formal","autonomy":"ai-led","tags":["number-theory","lean","formalization","fermat"],"humans":["Tianyi Peng"],"year_posed":1637,"sources":[{"label":"GitHub: anthropics/fermats-last-theorem","url":"https://github.com/anthropics/fermats-last-theorem","kind":"research"},{"label":"Anthropic: Formalizing Fermat's Last Theorem in Lean (PDF)","url":"https://www-cdn.anthropic.com/9e431dff043da6538d99d6c2d231b670aa3da263.pdf","kind":"research"},{"label":"Anthropic: Formalizing Fermat's Last Theorem","url":"https://www.anthropic.com/research/formalizing-fermats-last-theorem","kind":"announcement"},{"label":"Kevin Buzzard: FLT, Anthropic has beaten me to it","url":"https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/","kind":"commentary"}],"registrations":[{"registry":"mathdb","id":"316214","title":"Fermat's Last Theorem","url":"https://mathdb.com/p/316214/fermat-s-last-theorem","note":"Tracks the theorem itself rather than this formalization of it."}],"url":"https://whataifound.org/finding/2026-09-04-fermat-last-theorem-lean"},{"id":"2026-09-03-catalan-constant-irrationality","title":"Disputed claim that Catalan's constant is irrational","claim":"A preprint claims a proof that Catalan's constant is irrational, using weighted tails in the Calegari-Dimitrov-Tang framework; a specific technical objection to the argument has been raised publicly and is unresolved.","field":"mathematics","date":"2026-09-03","added":"2026-09-07","lab":"Nanjing University","model":"ChatGPT 5.6 Solar, named in the paper as the verifier; the model consulted during the work is named only as AI","verification":"disputed","autonomy":"ai-assisted","tags":["number-theory","irrationality","disputed","argument"],"humans":["Zhi-Wei Sun"],"sources":[{"label":"arXiv: Catalan's constant is irrational","url":"https://arxiv.org/abs/2609.04176","kind":"research"},{"label":"Hacker News: technical objection to the argument, equation 1.4 against equation 2.12","url":"https://news.ycombinator.com/item?id=49560333","kind":"challenge"},{"label":"arXiv: Wachs, A note on a recent claimed proof of the irrationality of Catalan's constant","url":"https://arxiv.org/abs/2609.22339","kind":"challenge"}],"url":"https://whataifound.org/finding/2026-09-03-catalan-constant-irrationality"},{"id":"2026-09-03-erdos-sos-conjecture","title":"Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement","claim":"A machine-checked Lean proof establishes the Erdos-Sos conjecture in the benchmark's formalization, which in one parity case assumes one more edge than the classical statement requires.","field":"mathematics","date":"2026-09-03","added":"2026-09-07","lab":"OpenAI / Epoch AI","model":"GPT-6 Astra (pre-release)","verification":"formal","autonomy":"autonomous","tags":["graph-theory","combinatorics","erdos","lean","formalization","argument"],"humans":["Tom Adamczewski"],"year_posed":1962,"sources":[{"label":"GitHub: tadamcz/erdos548, Lean proof and Palomar submission repository","url":"https://github.com/tadamcz/erdos548","kind":"research"},{"label":"vibemathed: Erdos Problem 548, the Erdos-Sos conjecture","url":"https://vibemathed.com/problem/erdos-problem-548-erdos-sos-conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"erdos-problem-548-erdos-sos-conjecture","url":"https://vibemathed.com/problem/erdos-problem-548-erdos-sos-conjecture"},{"registry":"mathdb","id":"392272","title":"Erdos-Sos conjecture","url":"https://mathdb.com/p/392272/erdos-sos-conjecture"}],"url":"https://whataifound.org/finding/2026-09-03-erdos-sos-conjecture"},{"id":"2026-09-03-koethe-conjecture-matrix-form","title":"Lean disproof of Krempa's matrix form of the Koethe conjecture","claim":"A machine-checked Lean proof refutes the matrix formulation that Krempa showed equivalent to the Koethe conjecture, found by a pre-release model with no human steering of the proof search.","field":"mathematics","date":"2026-09-03","added":"2026-09-07","lab":"OpenAI / Epoch AI","model":"GPT-6 Astra (pre-release)","verification":"formal","autonomy":"autonomous","tags":["algebra","ring-theory","lean","formalization","counterexample","construction"],"humans":["Tom Adamczewski"],"year_posed":1930,"sources":[{"label":"GitHub: tadamcz/koethe, Lean disproof and Palomar submission repository","url":"https://github.com/tadamcz/koethe","kind":"research"},{"label":"vibemathed: Koethe Conjecture","url":"https://vibemathed.com/problem/kothe-conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"kothe-conjecture","url":"https://vibemathed.com/problem/kothe-conjecture"}],"url":"https://whataifound.org/finding/2026-09-03-koethe-conjecture-matrix-form"},{"id":"2026-09-03-prime-gaps-212","title":"Bounded prime gaps improved to 212, with a Lean certificate of the deduction","claim":"Nine authors prove that infinitely many pairs of primes differ by at most 212, improving Stadlmann's 240, with the deduction certified in Lean by the group's own prover.","field":"mathematics","date":"2026-09-03","added":"2026-09-15","lab":"Axiom Math","model":"AxiomProver","verification":"claimed","autonomy":"collaborative","tags":["number-theory","prime-gaps","sieve-methods","lean","formalization","argument"],"humans":["Francois Charton","Letong Hong","Kenny Lau","Ken Ono","Guillaume Remy","Ho Chung Siu","Ashvin A. Swaminathan","Jesse Thorner","Yunzhou Xie"],"year_posed":1849,"sources":[{"label":"Axiom Math: a new bound for small gaps between primes (PDF)","url":"https://primegaps.axiommath.ai/bgp212.pdf","kind":"research"},{"label":"vibemathed: bounded prime gaps at most 212","url":"https://vibemathed.com/problem/bounded-prime-gaps-at-most-212","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"bounded-prime-gaps-at-most-212","url":"https://vibemathed.com/problem/bounded-prime-gaps-at-most-212"}],"url":"https://whataifound.org/finding/2026-09-03-prime-gaps-212"},{"id":"2026-09-03-smale-mean-value-k1","title":"Counterexample to Smale's mean value conjecture at K = 1","claim":"A Lean proof produced in an unsteered benchmark run disproves the \\(K = 1\\) form of Smale's 1981 mean value conjecture, exhibiting a polynomial for which no critical point meets the bound.","field":"mathematics","date":"2026-09-03","added":"2026-09-15","lab":"OpenAI / Epoch AI","model":"GPT-6 Astra (pre-release)","verification":"formal","autonomy":"autonomous","tags":["complex-analysis","polynomials","lean","formalization","construction"],"humans":["Tom Adamczewski"],"year_posed":1981,"sources":[{"label":"GitHub: tadamcz/mean-value-problem, the Lean 4 disproof","url":"https://github.com/tadamcz/mean-value-problem","kind":"research"},{"label":"vibemathed: Smale's mean value conjecture (K = 1)","url":"https://vibemathed.com/problem/smale-s-mean-value-conjecture-k-1","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"smale-s-mean-value-conjecture-k-1","url":"https://vibemathed.com/problem/smale-s-mean-value-conjecture-k-1"}],"url":"https://whataifound.org/finding/2026-09-03-smale-mean-value-k1"},{"id":"2026-09-02-daykin-frankl-conjecture","title":"Confirmation of the Daykin-Frankl conjecture from a language-model proof","claim":"A four-page note verifies and communicates a language-model-generated proof of the 1983 Daykin-Frankl conjecture on incomparable elements in convex subsets of the Boolean lattice.","field":"mathematics","date":"2026-09-02","added":"2026-09-07","lab":"Independent","model":"GPT-5.6 Sol Pro","verification":"author-verified","autonomy":"ai-led","tags":["combinatorics","boolean-lattice","order-theory","argument"],"humans":["Kada Williams"],"year_posed":1983,"sources":[{"label":"arXiv: Confirmation of the Daykin-Frankl conjecture","url":"https://arxiv.org/abs/2609.03087","kind":"research"},{"label":"vibemathed: The Daykin-Frankl conjecture on convex subsets of the Boolean lattice","url":"https://vibemathed.com/problem/daykin-frankl-conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"daykin-frankl-conjecture","url":"https://vibemathed.com/problem/daykin-frankl-conjecture"}],"url":"https://whataifound.org/finding/2026-09-02-daykin-frankl-conjecture"},{"id":"2026-09-02-prime-gaps-186","title":"Prime gaps at most 186, conditional on three unproved Lean axioms","claim":"An OpenAI repository derives a bound of 186 on infinitely many prime gaps in Lean, from three inputs it states as axioms rather than proving.","field":"mathematics","date":"2026-09-02","added":"2026-09-15","lab":"OpenAI","model":"GPT-6 Astra","verification":"claimed","autonomy":"ai-led","tags":["number-theory","prime-gaps","sieve-methods","lean","formalization","argument"],"year_posed":1849,"sources":[{"label":"GitHub: openai/PrimeGaps186, the conditional Lean formalization and numerical certificate","url":"https://github.com/openai/PrimeGaps186","kind":"research"},{"label":"vibemathed: prime gaps at most 186","url":"https://vibemathed.com/problem/prime-gaps-at-most-186","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"prime-gaps-at-most-186","url":"https://vibemathed.com/problem/prime-gaps-at-most-186"}],"url":"https://whataifound.org/finding/2026-09-02-prime-gaps-186"},{"id":"2026-09-02-qma2-oracle-separation","title":"A quantum oracle separating QMA(2) from QMA","claim":"A quantum oracle is constructed relative to which QMA(2) differs from QMA, resolving Watrous's no-disentanglers conjecture, from a proof idea the authors state was generated by a language model.","field":"computer-science","date":"2026-09-02","added":"2026-09-07","lab":"MIT / Columbia / University of Washington","model":"ChatGPT 5.6 Sol","verification":"author-verified","autonomy":"ai-assisted","tags":["quantum-computing","complexity-theory","oracle-separation","argument"],"humans":["John Bostanci","Sabee Grewal","Jonas Haferkamp","Andrew Huang","Yeongwoo Hwang","Anand Natarajan","Chinmay Nirkhe"],"year_posed":2009,"sources":[{"label":"arXiv: A quantum oracle separation between QMA(2) and QMA","url":"https://arxiv.org/abs/2609.02865","kind":"research"},{"label":"vibemathed: A quantum oracle separation between QMA(2) and QMA","url":"https://vibemathed.com/problem/a-quantum-oracle-separation-between-mathsf-qma-2-and-mathsf-qma","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"a-quantum-oracle-separation-between-mathsf-qma-2-and-mathsf-qma","url":"https://vibemathed.com/problem/a-quantum-oracle-separation-between-mathsf-qma-2-and-mathsf-qma"}],"url":"https://whataifound.org/finding/2026-09-02-qma2-oracle-separation"},{"id":"2026-09-02-trautman-conjecture","title":"A smooth counterexample to the Trautman conjecture","claim":"A strongly pseudoconvex CR three-manifold is constructed that carries a nowhere-zero closed section of its canonical bundle yet is not locally embeddable, disproving the Trautman conjecture.","field":"mathematics","date":"2026-09-02","added":"2026-09-07","lab":"Oklahoma State University","model":"ChatGPT Plus, version not named","verification":"author-verified","autonomy":"ai-assisted","tags":["differential-geometry","cr-geometry","counterexample","construction"],"humans":["Sean N. Curry"],"year_posed":1998,"sources":[{"label":"arXiv: A Smooth Counterexample to the Trautman Conjecture","url":"https://arxiv.org/abs/2609.03198","kind":"research"},{"label":"vibemathed: A smooth counterexample to the Trautman conjecture","url":"https://vibemathed.com/problem/a-smooth-counterexample-to-the-trautman-conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"a-smooth-counterexample-to-the-trautman-conjecture","url":"https://vibemathed.com/problem/a-smooth-counterexample-to-the-trautman-conjecture"}],"url":"https://whataifound.org/finding/2026-09-02-trautman-conjecture"},{"id":"2026-09-01-mckean-entropy-production","title":"Entropy production of the Boltzmann equation is not always monotone","claim":"Explicit radially symmetric mixtures of Maxwellians show the entropy production of the Boltzmann equation need not decrease monotonically, answering a question McKean asked in 1966.","field":"mathematics","date":"2026-09-01","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol; Claude","verification":"author-verified","autonomy":"ai-led","tags":["analysis","pde","mathematical-physics","counterexample"],"humans":["Luis Silvestre"],"year_posed":1966,"sources":[{"label":"arXiv: the entropy production is not always monotone for hard spheres or for Maxwell molecules","url":"https://arxiv.org/abs/2609.01753","kind":"research"},{"label":"vibemathed: McKean entropy-production conjecture","url":"https://vibemathed.com/problem/mckean-entropy-production-conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"mckean-entropy-production-conjecture","url":"https://vibemathed.com/problem/mckean-entropy-production-conjecture"}],"url":"https://whataifound.org/finding/2026-09-01-mckean-entropy-production"},{"id":"2026-09-01-saxl-common-neighbour","title":"Common neighbour conjectures for Saxl graphs fail at every base size","claim":"Primitive permutation groups are constructed whose generalised Saxl graphs contain two nonadjacent vertices with no common neighbour, disproving the Burness-Giudici conjecture and its extension at every base size.","field":"mathematics","date":"2026-09-01","added":"2026-09-03","lab":"Independent","model":"Codex; ChatGPT Pro; Claude","verification":"formal","autonomy":"collaborative","tags":["group-theory","combinatorics","counterexample","lean","formalization"],"humans":["Aluna Rizzoli","Adam R. Thomas"],"year_posed":2020,"sources":[{"label":"arXiv: common neighbour conjectures for Saxl graphs fail at every base size","url":"https://arxiv.org/abs/2609.01367","kind":"research"},{"label":"vibemathed: common neighbour conjectures for Saxl graphs","url":"https://vibemathed.com/problem/common-neighbour-conjectures-for-saxl-graphs","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"common-neighbour-conjectures-for-saxl-graphs","url":"https://vibemathed.com/problem/common-neighbour-conjectures-for-saxl-graphs"}],"url":"https://whataifound.org/finding/2026-09-01-saxl-common-neighbour"},{"id":"2026-08-31-boolean-multiplicative-complexity-mul4","title":"Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication","claim":"Multiplying two four-term binary polynomials needs exactly nine AND gates even when nonlinear intermediate wires may be reused, with the whole result formalized in Lean 4.","field":"computer-science","date":"2026-08-31","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol; Claude Opus 5","verification":"formal","autonomy":"ai-assisted","tags":["circuit-complexity","algorithms","lean","formalization"],"humans":["Gregory Morse"],"year_posed":2014,"sources":[{"label":"arXiv: unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication","url":"https://arxiv.org/abs/2608.30238","kind":"research"},{"label":"vibemathed: unrestricted Boolean multiplicative complexity of Mul4","url":"https://vibemathed.com/problem/unrestricted-multiplicative-complexity-mul4","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"unrestricted-multiplicative-complexity-mul4","url":"https://vibemathed.com/problem/unrestricted-multiplicative-complexity-mul4"},{"registry":"palomar","id":"PALOMAR-2026-09-21-000005","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-09-21-000005&version=1","repository":"GregoryMorse/unrestricted-boolean-mul","commit":"56837b8ed4ffe6390a7a84d9a77f1489bfd9d872","theorems":["UnrestrictedBooleanMul.mc_mul_zero","UnrestrictedBooleanMul.mc_mul_one","UnrestrictedBooleanMul.mc_mul_two","UnrestrictedBooleanMul.mc_mul_three","UnrestrictedBooleanMul.N4.no_eight_gate_circuit","UnrestrictedBooleanMul.N4.mc_mul_four"],"checked":"2026-09-21","note":"Registered by the author. Palomar's record states that the open unrestricted and bilinear lower bounds for five and six terms are not claims of this submission."}],"url":"https://whataifound.org/finding/2026-08-31-boolean-multiplicative-complexity-mul4"},{"id":"2026-08-31-pisot-cantor-equidistribution","title":"Criteria and two quadratic instances for Bugeaud's Problem 10.61","claim":"Covering criteria for a 1967 equidistribution problem of Mendès France are proved and applied to two quadratic Pisot cases, with Lean checking; the general problem stays open.","field":"mathematics","date":"2026-08-31","added":"2026-09-03","lab":"Independent","model":"Claude Fable 5; Claude Opus 5","verification":"claimed","autonomy":"ai-led","tags":["number-theory","equidistribution","lean","partial-result"],"humans":["Ralf Stephan"],"year_posed":1967,"sources":[{"label":"GitHub: Pisot-Cantor-61, paper and Lean development","url":"https://github.com/rwst/Pisot-Cantor-61","kind":"research"},{"label":"vibemathed: Bugeaud Problem 10.61","url":"https://vibemathed.com/problem/bugeaud-problem-10-61","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"bugeaud-problem-10-61","url":"https://vibemathed.com/problem/bugeaud-problem-10-61"},{"registry":"palomar","id":"PALOMAR-2026-08-31-000013","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-08-31-000013&version=2","repository":"rwst/Pisot-Cantor-61","commit":"d61132ffcdb748b641f9de59b7acfffc860796b2","theorems":["BB61.QuadSetup.equidistributed_iff_exists_invariant_measure","BB61.QuadSetup.forall_not_equidistributed_iff_exists_trigCertificate","MeasureTheory.le_integral_of_partitionPressure_le","BB61.forall_not_equidistributed_of_partitionPressure_lt","BB61.forall_not_equidistributed_of_transferBound","BB61.QuadSetup.routeAExponent_mul_hMin","BB61.slope_neg_iff","BB61.logb_coverTotal_balancedDepth_le","BB61.QuadSetup.exists_avoided_interval","BB61.QuadSetup.not_equidistributed_of_routeAExponent_lt_one","BB61.QuadSetup.routeAExponent_lt_one_iff_quadratic","BB61.isPisot_family","BB61.norm_le_familyConjBound","BB61.routeA_family_lt_one","BB61.routeA_two_add_sqrt5","BB61.two_add_sqrt5_not_equidistributed","BB61.GapThree.problem_10_61_two_add_sqrt3_axiom_free"],"checked":"2026-09-06","note":"What typechecks is the criteria and the two quadratic instances, not Problem 10.61. BB61.QuadSetup.routeAExponent_lt_one_iff_quadratic is where that boundary is visible: the covering criterion is characterized only for quadratic setups, and the arbitrary-degree material carries no compared statement to the problem. Every compared statement depends on propext, Classical.choice and Quot.sound and nothing else. Palomar also carries the submitter's own disclosure that he has not verified informal-to-formal fidelity, and that the challenge file governs wherever the prose disagrees with it."}],"url":"https://whataifound.org/finding/2026-08-31-pisot-cantor-equidistribution"},{"id":"2026-08-31-stable-forking","title":"Counterexample to the stable forking conjecture","claim":"A simple first-order theory is constructed in which forking cannot always be witnessed by a stable formula, answering a question of Hart, Kim and Pillay open since 1996.","field":"mathematics","date":"2026-08-31","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol","verification":"author-verified","autonomy":"collaborative","tags":["model-theory","logic","counterexample","construction"],"humans":["James Freitag","Scott Mutchnik"],"year_posed":1996,"sources":[{"label":"arXiv: a counterexample to the stable forking conjecture","url":"https://arxiv.org/abs/2609.00436","kind":"research"},{"label":"vibemathed: a counterexample to the stable forking conjecture","url":"https://vibemathed.com/problem/a-counterexample-to-the-stable-forking-conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"a-counterexample-to-the-stable-forking-conjecture","url":"https://vibemathed.com/problem/a-counterexample-to-the-stable-forking-conjecture"},{"registry":"mathdb","id":"375925","title":"The stable forking conjecture","url":"https://mathdb.com/p/375925/the-stable-forking-conjecture"}],"url":"https://whataifound.org/finding/2026-08-31-stable-forking"},{"id":"2026-08-29-dean-conjecture-k5","title":"Dean's conjecture for k = 5, cycles of length divisible by five","claim":"A preprint claims every finite simple graph of minimum degree at least five contains a cycle whose length is divisible by five, the last open case of Dean's 1988 conjecture.","field":"mathematics","date":"2026-08-29","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol; Claude Opus 5; GLM 5.3 Flash","verification":"claimed","autonomy":"ai-led","tags":["graph-theory","combinatorics","computer-assisted","argument"],"humans":["Elias Botsford"],"year_posed":1988,"sources":[{"label":"Zenodo: cycles of length divisible by five in graphs of minimum degree five","url":"https://zenodo.org/records/22182448","kind":"research"},{"label":"Zenodo: computational supplement, version 1.0.1","url":"https://doi.org/10.5281/zenodo.22167084","kind":"research"},{"label":"vibemathed: Dean's conjecture for k = 5","url":"https://vibemathed.com/problem/dean-s-conjecture-for-k-5","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"dean-s-conjecture-for-k-5","url":"https://vibemathed.com/problem/dean-s-conjecture-for-k-5"},{"registry":"mathdb","id":"374541","title":"Dean's conjecture on cycles divisible by the minimum degree","url":"https://mathdb.com/p/374541/dean-s-conjecture-on-cycles-divisible-by-the-minimum-degree","note":"Names the same three models this entry credits and records k = 5 as the last open case, which is the framing the entry rests on."}],"url":"https://whataifound.org/finding/2026-08-29-dean-conjecture-k5"},{"id":"2026-08-29-metric-distortion-23282","title":"Randomized metric distortion improved to 2.3282","claim":"A randomized voting rule built on a new random-size stable lottery achieves metric distortion 2.3282, past a 2.5 barrier that existing arguments could not cross.","field":"computer-science","date":"2026-08-29","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol; Claude Opus 5.0","verification":"author-verified","autonomy":"ai-led","tags":["algorithms","social-choice","game-theory","argument"],"humans":["Nisarg Shah"],"sources":[{"label":"arXiv: improving randomized metric distortion to 2.3282","url":"https://arxiv.org/abs/2608.29308","kind":"research"},{"label":"vibemathed: improving randomized metric distortion to 2.3282","url":"https://vibemathed.com/problem/improving-randomized-metric-distortion-to-2-3282","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"improving-randomized-metric-distortion-to-2-3282","url":"https://vibemathed.com/problem/improving-randomized-metric-distortion-to-2-3282"}],"url":"https://whataifound.org/finding/2026-08-29-metric-distortion-23282"},{"id":"2026-08-28-percolation-critical-point","title":"Lean proof that the percolation probability vanishes at the critical point in every dimension","claim":"A Lean development proves that nearest-neighbour Bernoulli bond percolation on the integer lattice has no infinite cluster at its critical parameter in every dimension at least two, which would settle the dimensions 3 to 10 that were open.","field":"mathematics","date":"2026-08-28","added":"2026-09-07","lab":"Anthropic","model":"Anthropic Claude models, versions not stated","verification":"claimed","autonomy":"ai-led","tags":["probability","percolation","lean","formalization","argument"],"humans":["Justin Leder"],"sources":[{"label":"GitHub: anthropics/formal-math, percolation project at the pinned commit 795efb86","url":"https://github.com/anthropics/formal-math/tree/795efb86f191735c5481675763537cfb4ff37e55/percolation","kind":"research"},{"label":"Audit record for the percolation project","url":"https://github.com/anthropics/formal-math/blob/795efb86f191735c5481675763537cfb4ff37e55/percolation/AUDIT.md","kind":"research"},{"label":"arXiv: Kozma and Nitzan, gluing inequalities for percolation","url":"https://arxiv.org/abs/2401.12397","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"absence-of-critical-bernoulli-bond-percolation-on-z-d-in-every-dimension-d-2","url":"https://vibemathed.com/problem/absence-of-critical-bernoulli-bond-percolation-on-z-d-in-every-dimension-d-2","note":"Registered on 2026-09-03 under a different title, against the same pinned commit 795efb86 this entry cites. Rated lean-verified but review pending."}],"url":"https://whataifound.org/finding/2026-08-28-percolation-critical-point"},{"id":"2026-08-27-entanglement-supporting-functional","title":"Supporting affine functionals for entanglement of formation need not exist","claim":"An explicit two-qubit state has no global supporting affine functional for the entanglement of formation, contradicting an assumption used in several papers.","field":"physics","date":"2026-08-27","added":"2026-09-03","lab":"Independent","model":"Claude Fable 5","verification":"author-verified","autonomy":"ai-assisted","tags":["quantum-information","entanglement","counterexample"],"humans":["A. S. Holevo","M. E. Shirokov"],"sources":[{"label":"arXiv: on supporting affine functionals for entanglement of formation","url":"https://arxiv.org/abs/2608.27363","kind":"research"},{"label":"vibemathed: supporting affine functionals for entanglement of formation","url":"https://vibemathed.com/problem/supporting-affine-functionals-for-entanglement-of-formation","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"supporting-affine-functionals-for-entanglement-of-formation","url":"https://vibemathed.com/problem/supporting-affine-functionals-for-entanglement-of-formation"}],"url":"https://whataifound.org/finding/2026-08-27-entanglement-supporting-functional"},{"id":"2026-08-27-intuitionistic-higher-order-truth","title":"Not every Heyting algebra is the subterminal lattice of a topos","claim":"The free Heyting algebra on two generators cannot be the lattice of subterminal objects of an elementary topos, answering the question in the negative.","field":"mathematics","date":"2026-08-27","added":"2026-09-03","lab":"Independent","model":"ChatGPT 5.6 Sol","verification":"author-verified","autonomy":"ai-assisted","tags":["logic","category-theory","counterexample"],"humans":["Lingyuan Ye","Yiqi Xu"],"sources":[{"label":"arXiv: failure of higher-order truth within intuitionistic propositional logic","url":"https://arxiv.org/abs/2608.26874","kind":"research"},{"label":"vibemathed: failure of higher-order truth within intuitionistic propositional logic","url":"https://vibemathed.com/problem/failure-of-higher-order-truth-within-intuitionistic-propositional-logic","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"failure-of-higher-order-truth-within-intuitionistic-propositional-logic","url":"https://vibemathed.com/problem/failure-of-higher-order-truth-within-intuitionistic-propositional-logic"}],"url":"https://whataifound.org/finding/2026-08-27-intuitionistic-higher-order-truth"},{"id":"2026-08-27-large-systoles","title":"Hyperbolic surfaces with large systoles in every large genus","claim":"For every sufficiently large genus there is a closed hyperbolic surface whose systole is at least \\(\\log g - 12\\log\\log g\\), raising the known asymptotic constant from 2/9 to 1.","field":"mathematics","date":"2026-08-27","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol","verification":"author-verified","autonomy":"ai-led","tags":["geometry","hyperbolic-geometry","construction"],"humans":["Yifei Cai"],"sources":[{"label":"arXiv: a note on surfaces with large systoles","url":"https://arxiv.org/abs/2608.26660","kind":"research"},{"label":"vibemathed: large systoles in every sufficiently large genus","url":"https://vibemathed.com/problem/large-systoles-in-every-sufficiently-large-genus","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"large-systoles-in-every-sufficiently-large-genus","url":"https://vibemathed.com/problem/large-systoles-in-every-sufficiently-large-genus"}],"url":"https://whataifound.org/finding/2026-08-27-large-systoles"},{"id":"2026-08-27-norm-variation-ergodic-averages-lean","title":"Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week","claim":"A Lean 4 proof of about 107,000 lines of a new norm-variation estimate for multiple ergodic averages of commuting transformations, which strengthens Tao's 2008 norm-convergence theorem, was produced by coding agents in one week from a human-written blueprint and hand-formalized statements.","field":"mathematics","date":"2026-08-27","added":"2026-09-28","lab":"Independent","model":"Coding agents, models not stated","verification":"author-verified","autonomy":"ai-led","tags":["ergodic-theory","harmonic-analysis","lean","formalization"],"humans":["Floris van Doorn","Polona Durcik","Joris Roos","Lenka Slavíková","Christoph Thiele"],"sources":[{"label":"arXiv: A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations","url":"https://arxiv.org/abs/2608.27321","kind":"research"},{"label":"GitHub: roos-j/lean-nct","url":"https://github.com/roos-j/lean-nct","kind":"research"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-09-15-000008","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-09-15-000008&version=1","repository":"roos-j/lean-nct","commit":"3e09aa52c478ec69abb02eb250c5e5ed06653c3a","theorems":["nCT.main_ergodic_theorem","nCT.tao_norm_convergence","nCT.main_twisted_theorem"],"checked":"2026-09-15"}],"url":"https://whataifound.org/finding/2026-08-27-norm-variation-ergodic-averages-lean"},{"id":"2026-08-26-nevanlinna-half-plane","title":"Counterexample to Nevanlinna's half-plane omitted-values question","claim":"An explicit meromorphic function omits three values in a half-plane without being of bounded type there, answering in the negative a question of Nevanlinna open for more than a century.","field":"mathematics","date":"2026-08-26","added":"2026-08-31","lab":"Independent","model":"GPT-5.6 Sol Ultra","verification":"author-verified","autonomy":"ai-led","tags":["complex-analysis","value-distribution","counterexample","construction"],"humans":["Quanyu Tang","Bokai Cui","Wei He","Tao Hu","Yanyang Li","Ke Wang","Zijun Yu"],"sources":[{"label":"arXiv: Three omitted values and non-Blaschke point divisors in half-planes","url":"https://arxiv.org/abs/2608.26062","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"nevanlinna-s-half-plane-omitted-values-problem","url":"https://vibemathed.com/problem/nevanlinna-s-half-plane-omitted-values-problem"},{"registry":"mathdb","id":"392094","title":"Nevanlinna's half-plane problem","url":"https://mathdb.com/p/392094/nevanlinna-s-half-plane-problem","note":"Tracks the identical claimed counterexample to the same century-old problem."}],"url":"https://whataifound.org/finding/2026-08-26-nevanlinna-half-plane"},{"id":"2026-08-26-spin-systems-girth-five","title":"Rapid mixing for spin systems on graphs of girth at least five","claim":"Glauber dynamics for proper \\(q\\)-colourings mixes rapidly once \\(q\\) exceeds the maximum degree by any fixed factor, provided the graph has girth at least five.","field":"computer-science","date":"2026-08-26","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol Ultra","verification":"author-verified","autonomy":"collaborative","tags":["algorithms","sampling","markov-chains","combinatorics","argument"],"humans":["Xiaoyu Chen","Kuikui Liu"],"year_posed":1995,"sources":[{"label":"arXiv: a spectral local-to-global principle for spin systems on graphs with girth at least five","url":"https://arxiv.org/abs/2608.25491","kind":"research"},{"label":"vibemathed: rapid mixing for spin systems on graphs of girth at least five","url":"https://vibemathed.com/problem/rapid-mixing-for-spin-systems-on-graphs-of-girth-at-least-five","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"rapid-mixing-for-spin-systems-on-graphs-of-girth-at-least-five","url":"https://vibemathed.com/problem/rapid-mixing-for-spin-systems-on-graphs-of-girth-at-least-five"}],"url":"https://whataifound.org/finding/2026-08-26-spin-systems-girth-five"},{"id":"2026-08-25-erdos-4-prime-gaps","title":"Improved lower bound for large gaps between consecutive primes","claim":"A new sieving construction raises the record lower bound on how large the gap between consecutive primes becomes infinitely often, the first advance on Erdős Problem #4 since 2018.","field":"mathematics","date":"2026-08-25","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol","verification":"independent","autonomy":"ai-led","tags":["number-theory","erdos","prime-gaps","sieve-methods","construction"],"humans":["DottedCalculator","Boris Alexeev"],"year_posed":1955,"sources":[{"label":"Manuscript: Erdős_4_GPT_5.6_Sol.pdf","url":"https://github.com/DottedCalculator/ai-math/blob/main/Erdos_4_GPT_5.6_Sol.pdf","kind":"research"},{"label":"Erdős Problems: problem #4","url":"https://www.erdosproblems.com/4","kind":"commentary"},{"label":"vibemathed: a tilted residue-class construction for long prime-free intervals","url":"https://vibemathed.com/problem/tilted-residue-class-construction-for-long-prime-free-intervals","kind":"commentary"},{"label":"Jared Duker Lichtman on the result (X)","url":"https://x.com/jdlichtman/status/2094040463443673227","kind":"announcement"}],"registrations":[{"registry":"vibemathed","id":"tilted-residue-class-construction-for-long-prime-free-intervals","url":"https://vibemathed.com/problem/tilted-residue-class-construction-for-long-prime-free-intervals"}],"url":"https://whataifound.org/finding/2026-08-25-erdos-4-prime-gaps"},{"id":"2026-08-25-froberg-quintics-septics","title":"Fröberg's conjecture for quintics and septics in four variables","claim":"Fröberg's predicted Hilbert series is proved for ideals generated by any number of general forms of degree five or seven in four variables.","field":"mathematics","date":"2026-08-25","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol; Claude Fable 5; Grok 4.6","verification":"author-verified","autonomy":"collaborative","tags":["algebra","commutative-algebra","computer-assisted"],"humans":["Qihang Wang","Dongming Zhang"],"year_posed":1985,"sources":[{"label":"arXiv: Fröberg's conjecture for quintics and septics in four variables","url":"https://arxiv.org/abs/2608.24797","kind":"research"},{"label":"vibemathed: Fröberg's conjecture for quintics and septics in four variables","url":"https://vibemathed.com/problem/froberg-s-conjecture-for-quintics-and-septics-in-four-variables","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"froberg-s-conjecture-for-quintics-and-septics-in-four-variables","url":"https://vibemathed.com/problem/froberg-s-conjecture-for-quintics-and-septics-in-four-variables"}],"url":"https://whataifound.org/finding/2026-08-25-froberg-quintics-septics"},{"id":"2026-08-25-generically-stable-keisler","title":"Equivalence of generic stability notions for Keisler measures","claim":"Three candidate definitions of generic stability for a Borel-definable global Keisler measure are shown to be equivalent, closing a research objective left open by earlier work.","field":"mathematics","date":"2026-08-25","added":"2026-09-03","lab":"Independent","model":"ChatGPT 5.5; ChatGPT 5.6 Sol; Kimi K3; Claude Fable 5","verification":"author-verified","autonomy":"ai-led","tags":["model-theory","logic","argument"],"humans":["Gabriel Conant","Kyle Gannon","James E. Hanson"],"year_posed":2020,"sources":[{"label":"arXiv: generically stable Keisler measures","url":"https://arxiv.org/abs/2608.24605","kind":"research"},{"label":"vibemathed: equivalence of generic stability notions for Keisler measures","url":"https://vibemathed.com/problem/equivalence-of-generic-stability-notions-for-keisler-measures","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"equivalence-of-generic-stability-notions-for-keisler-measures","url":"https://vibemathed.com/problem/equivalence-of-generic-stability-notions-for-keisler-measures"}],"url":"https://whataifound.org/finding/2026-08-25-generically-stable-keisler"},{"id":"2026-08-25-ramsey-algebraic-construction","title":"Improved algebraic construction for off-diagonal Ramsey numbers","claim":"A finite-geometry construction supplied by a language model, then reworked by the authors, improves the explicit lower bound for off-diagonal Ramsey numbers.","field":"mathematics","date":"2026-08-25","added":"2026-08-31","lab":"Independent","model":"ChatGPT 5.6","verification":"author-verified","autonomy":"ai-assisted","tags":["combinatorics","ramsey-theory","finite-geometry","construction"],"humans":["Ferdinand Ihringer","Sam Mattheus"],"sources":[{"label":"arXiv: An improved algebraic construction for Ramsey numbers","url":"https://arxiv.org/abs/2608.21769","kind":"research"}],"url":"https://whataifound.org/finding/2026-08-25-ramsey-algebraic-construction"},{"id":"2026-08-25-sparse-convex-body-domination","title":"Sparse domination implies convex body domination","claim":"Any bilinear form with a sparse bound has a convex body sparse bound for its vector-valued extension, answering a question about the relation between the two notions.","field":"mathematics","date":"2026-08-25","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol Pro","verification":"author-verified","autonomy":"ai-assisted","tags":["analysis","harmonic-analysis","argument"],"humans":["Aapo Laukkarinen","Emiel Lorist"],"year_posed":2017,"sources":[{"label":"arXiv: sparse domination implies convex body domination","url":"https://arxiv.org/abs/2608.24802","kind":"research"},{"label":"vibemathed: sparse domination implies convex body domination","url":"https://vibemathed.com/problem/sparse-domination-implies-convex-body-domination","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"sparse-domination-implies-convex-body-domination","url":"https://vibemathed.com/problem/sparse-domination-implies-convex-body-domination"}],"url":"https://whataifound.org/finding/2026-08-25-sparse-convex-body-domination"},{"id":"2026-08-24-ancheta-massey-linear-coding","title":"Optimal linear encoding rate for lossy compression of Bernoulli sources","claim":"Ancheta's answer to Massey's question about linear encoders for lossy compression is extended from the fair-coin case to every source bias below one half.","field":"computer-science","date":"2026-08-24","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol","verification":"author-verified","autonomy":"ai-led","tags":["information-theory","coding-theory","argument"],"humans":["Yihong Wu"],"year_posed":1978,"sources":[{"label":"arXiv: entropy of Bernoulli measures conditioned on affine subspaces and a problem of Ancheta-Massey","url":"https://arxiv.org/abs/2608.22837","kind":"research"},{"label":"vibemathed: entropy of Bernoulli measures conditioned on affine subspaces","url":"https://vibemathed.com/problem/entropy-of-bernoulli-measures-conditioned-on-affine-subspaces-and-a-problem-of-a","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"entropy-of-bernoulli-measures-conditioned-on-affine-subspaces-and-a-problem-of-a","url":"https://vibemathed.com/problem/entropy-of-bernoulli-measures-conditioned-on-affine-subspaces-and-a-problem-of-a"}],"url":"https://whataifound.org/finding/2026-08-24-ancheta-massey-linear-coding"},{"id":"2026-08-23-elliptic-rank-31","title":"Elliptic curves over the rationals of rank at least 30 and at least 31","claim":"Two explicit elliptic curves over the rationals carry 30 and 31 independent rational points, raising the Mordell-Weil rank record twice in four days.","field":"mathematics","date":"2026-08-23","added":"2026-09-03","lab":"Independent","model":"Claude","verification":"claimed","autonomy":"ai-assisted","tags":["number-theory","elliptic-curves","record","search"],"humans":["Levent Alpöge","Ava Howell"],"sources":[{"label":"Elliptic curve rank leaderboard: curve 302, rank at least 31","url":"https://elliptic-rank.icarm.cloud/curve/302","kind":"research"},{"label":"Elliptic curve rank leaderboard: curve 273, rank at least 30","url":"https://elliptic-rank.icarm.cloud/curve/273","kind":"research"},{"label":"vibemathed: a rank-31 record for an elliptic curve over Q","url":"https://vibemathed.com/problem/elliptic-curve-rank-record-thirty-one","kind":"commentary"},{"label":"vibemathed: record rank for an elliptic curve over Q","url":"https://vibemathed.com/problem/elliptic-curve-rank-record-thirty","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"elliptic-curve-rank-record-thirty-one","url":"https://vibemathed.com/problem/elliptic-curve-rank-record-thirty-one"},{"registry":"vibemathed","id":"elliptic-curve-rank-record-thirty","url":"https://vibemathed.com/problem/elliptic-curve-rank-record-thirty"}],"url":"https://whataifound.org/finding/2026-08-23-elliptic-rank-31"},{"id":"2026-08-23-s6-complex-structure","title":"A complex structure on the six-sphere","claim":"An explicit compact complex threefold, built as a family of 2-tori over the \\((3, 4, \\infty)\\) orbifold, is diffeomorphic to the six-sphere, which settles the question Hopf raised in 1948 of whether the six-sphere admits a complex structure.","field":"mathematics","date":"2026-08-23","added":"2026-08-25","lab":"Anthropic","model":"Claude, version not stated","verification":"independent","autonomy":"ai-assisted","tags":["complex-geometry","differential-geometry","hopf-problem","construction","contested"],"humans":["Levent Alpöge"],"year_posed":1948,"sources":[{"label":"Alpöge: The (3,4,infinity) modular family of 2-tori is a complex structure on S⁶ (PDF)","url":"https://alpo.ge/s6.pdf","kind":"research"},{"label":"Coverage: officechai","url":"https://officechai.com/ai/anthropic-researcher-says-claude-helped-build-a-complex-structure-on-s%E2%81%B6-taking-aim-at-the-unsolved-hopf-problem/","kind":"coverage"},{"label":"Levent Alpöge, announcement (X)","url":"https://x.com/__alpoge__/status/2091639597193368014","kind":"announcement"},{"label":"GitHub: plby/HopfProblem, Boris Alexeev's Lean formalization","url":"https://github.com/plby/HopfProblem","kind":"research"},{"label":"Philip Engel: Complex structures on S6, a self-contained proof (PDF)","url":"https://philip-engel.github.io/S6.pdf","kind":"commentary"},{"label":"Quanta Magazine: update on the six-sphere, with Engel and Abouzaid on checking it","url":"https://www.quantamagazine.org/updates/transformation/#167201","kind":"coverage"},{"label":"Scientific American: AI solves 79-year-old math mystery of six-dimensional spheres","url":"https://www.scientificamerican.com/article/ai-solves-79-year-old-math-mystery-of-six-dimensional-spheres/","kind":"coverage"}],"registrations":[{"registry":"vibemathed","id":"modular-family-of-2-tori-as-a-complex-structure-on-s6","url":"https://vibemathed.com/problem/modular-family-of-2-tori-as-a-complex-structure-on-s6"}],"url":"https://whataifound.org/finding/2026-08-23-s6-complex-structure"},{"id":"2026-08-22-erdos-270-affine-transcendence","title":"Transcendence in the affine case of Erdős Problem 270","claim":"The series in Erdős Problem 270 is claimed transcendental for every positive integer-valued affine choice of the defining function.","field":"mathematics","date":"2026-08-22","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol (Codex)","verification":"claimed","autonomy":"ai-led","tags":["number-theory","erdos","transcendence","lean"],"year_posed":1980,"sources":[{"label":"GitHub: algebraic independence in the affine case of Erdős Problem 270","url":"https://github.com/clambro/erdos-270-transcendence","kind":"research"},{"label":"Erdős Problems: problem #270","url":"https://www.erdosproblems.com/270","kind":"commentary"},{"label":"vibemathed: transcendence in the affine case of Erdős Problem 270","url":"https://vibemathed.com/problem/transcendence-in-the-affine-case-of-erdos-problem-270","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"transcendence-in-the-affine-case-of-erdos-problem-270","url":"https://vibemathed.com/problem/transcendence-in-the-affine-case-of-erdos-problem-270"}],"url":"https://whataifound.org/finding/2026-08-22-erdos-270-affine-transcendence"},{"id":"2026-08-21-bounded-mass-property","title":"Counterexample to the bounded mass property on the Hopf threefold","claim":"The bounded mass property fails on the Hopf threefold, answering a question of Boucksom, Guedj and Lu.","field":"mathematics","date":"2026-08-21","added":"2026-09-03","lab":"Independent","model":"Rethlas agent (GPT-5.6 Sol)","verification":"author-verified","autonomy":"ai-led","tags":["geometry","complex-geometry","counterexample"],"humans":["Mingchen Xia","Kewei Zhang"],"year_posed":2025,"sources":[{"label":"arXiv: a counterexample to the bounded mass property","url":"https://arxiv.org/abs/2608.21053","kind":"research"},{"label":"vibemathed: bounded mass property for compact complex manifolds","url":"https://vibemathed.com/problem/bounded-mass-property-for-compact-complex-manifolds","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"bounded-mass-property-for-compact-complex-manifolds","url":"https://vibemathed.com/problem/bounded-mass-property-for-compact-complex-manifolds"}],"url":"https://whataifound.org/finding/2026-08-21-bounded-mass-property"},{"id":"2026-08-21-dubickas-square-roots","title":"Dubickas's question on integral parts of powers of square roots settled","claim":"The square root of 3 admits a real multiplier making every integral part of its powers even, and among integers only the square root of 2 fails to, answering a question Dubickas posed in 2006 and classifying the whole square-root case.","field":"mathematics","date":"2026-08-21","added":"2026-08-25","lab":"Independent","model":"Claude Fable 5 and Claude Opus 5","verification":"formal","autonomy":"ai-led","tags":["lean","formalization","number-theory","z-numbers","argument"],"humans":["Ralf Stephan"],"year_posed":2006,"sources":[{"label":"Even integral parts of powers of square roots (ResearchGate)","url":"https://www.researchgate.net/publication/413520035_Even_integral_parts_of_powers_of_square_roots","kind":"research"},{"label":"Lean development: rwst/Square-Roots","url":"https://github.com/rwst/Square-Roots","kind":"research"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-08-23-000002","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-08-23-000002&version=1","repository":"rwst/Square-Roots","commit":"e3184902f13967b9f20f37244b3d1c30610ca846","theorems":["SZ.sqrtThree_mem_MahlerZ","SZ.sqrtThree_notMem_S","SZ.sqrt_natCast_mem_S_iff"],"checked":"2026-08-23","note":"Eleven modules, no unfinished proof steps and no declared axioms beyond the three standard ones."}],"url":"https://whataifound.org/finding/2026-08-21-dubickas-square-roots"},{"id":"2026-08-21-scl-relator-invariance","title":"Stable commutator length of a relator is not a one-relator group invariant","claim":"Two explicit words give isomorphic one-relator groups whose relators have different stable commutator lengths, answering a question of Heuer and Loh in the negative.","field":"mathematics","date":"2026-08-21","added":"2026-09-03","lab":"Independent","model":"Claude Opus 5; Harmonic Aristotle","verification":"author-verified","autonomy":"ai-assisted","tags":["group-theory","geometric-group-theory","counterexample","computer-assisted"],"humans":["Artem Semidetnov"],"year_posed":2019,"sources":[{"label":"arXiv: the stable commutator length of a relator is not a one-relator group invariant","url":"https://arxiv.org/abs/2608.21465","kind":"research"},{"label":"vibemathed: the stable commutator length of a relator is not a one-relator group invariant","url":"https://vibemathed.com/problem/the-stable-commutator-length-of-a-relator-is-not-a-one-relator-group-invariant","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"the-stable-commutator-length-of-a-relator-is-not-a-one-relator-group-invariant","url":"https://vibemathed.com/problem/the-stable-commutator-length-of-a-relator-is-not-a-one-relator-group-invariant"}],"url":"https://whataifound.org/finding/2026-08-21-scl-relator-invariance"},{"id":"2026-08-20-fast-dynamo-three-torus","title":"A smooth random fast dynamo on the three-torus","claim":"A random smooth divergence-free velocity field on the three-torus is constructed whose magnetic field grows exponentially at a rate bounded below independently of the resistivity.","field":"mathematics","date":"2026-08-20","added":"2026-09-03","lab":"Independent","model":"ChatGPT 5.6 Sol Ultra","verification":"author-verified","autonomy":"ai-led","tags":["analysis","pde","probability","construction"],"humans":["Keefer Rowan"],"sources":[{"label":"arXiv: an AI-discovered smooth random fast dynamo on T³","url":"https://arxiv.org/abs/2608.20105","kind":"research"},{"label":"vibemathed: smooth random fast dynamo on the three-torus","url":"https://vibemathed.com/problem/smooth-random-fast-dynamo-on-the-three-torus","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"smooth-random-fast-dynamo-on-the-three-torus","url":"https://vibemathed.com/problem/smooth-random-fast-dynamo-on-the-three-torus"}],"url":"https://whataifound.org/finding/2026-08-20-fast-dynamo-three-torus"},{"id":"2026-08-20-marton-inner-bound","title":"Marton's inner bound shown not to reach the broadcast channel capacity region","claim":"There are discrete memoryless broadcast channels whose capacity region is strictly larger than Marton's inner bound, settling in the negative a question open since 1979.","field":"computer-science","date":"2026-08-20","added":"2026-08-21","lab":"Independent","model":"GPT-5.6 Sol, Claude Fable 5 and Claude Opus 5","verification":"author-verified","autonomy":"ai-assisted","tags":["information-theory","broadcast-channel","counterexample","construction"],"humans":["Mian Huang","Yanxiao Liu","Yi Liu"],"year_posed":1979,"sources":[{"label":"arXiv: Sub-optimality of Marton's Inner Bound for the Two-Receiver Broadcast Channel","url":"https://arxiv.org/abs/2608.19869","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"marton-inner-bound-capacity-region","url":"https://vibemathed.com/problem/marton-inner-bound-capacity-region"},{"registry":"mathdb","id":"390544","title":"Marton's conjecture on broadcast-channel capacity","url":"https://mathdb.com/p/390544/marton-s-conjecture-on-broadcast-channel-capacity","note":"MathDB records the same three models and describes the result as remaining unverified as a theorem, which matches the caveat this entry already carries."}],"url":"https://whataifound.org/finding/2026-08-20-marton-inner-bound"},{"id":"2026-08-20-pauli-fractional-colouring","title":"Counterexamples to the fractional colouring conjecture for Pauli shadow tomography","claim":"The fractional chromatic number of the anticommutation graph of large-expectation Pauli observables is not bounded by a constant over \\(\\varepsilon^2\\), removing a proposed route to triply efficient shadow tomography.","field":"physics","date":"2026-08-20","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol","verification":"author-verified","autonomy":"collaborative","tags":["quantum-information","combinatorics","counterexample"],"humans":["Jędrzej Stempin","Santiago Llorens","Felix Huber"],"year_posed":2025,"sources":[{"label":"arXiv: counterexamples to the fractional coloring conjecture for triply efficient shadow tomography","url":"https://arxiv.org/abs/2608.20113","kind":"research"},{"label":"vibemathed: the fractional colouring conjecture for triply efficient Pauli shadow tomography","url":"https://vibemathed.com/problem/fractional-colouring-pauli-shadow-tomography","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"fractional-colouring-pauli-shadow-tomography","url":"https://vibemathed.com/problem/fractional-colouring-pauli-shadow-tomography"}],"url":"https://whataifound.org/finding/2026-08-20-pauli-fractional-colouring"},{"id":"2026-08-19-big-line-big-clique","title":"First open case of the big-line-big-clique conjecture","claim":"Every finite point set of size at least \\(10^{11055931}\\) contains four collinear points or six points that pairwise see each other, settling the first open case of the Kára-Pór-Wood conjecture.","field":"mathematics","date":"2026-08-19","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol Pro","verification":"author-verified","autonomy":"ai-led","tags":["combinatorics","discrete-geometry","argument"],"humans":["Édouard Bonnet"],"year_posed":2005,"sources":[{"label":"arXiv: large finite point sets have 4 collinear points or a 6-clique","url":"https://arxiv.org/abs/2608.19468","kind":"research"},{"label":"vibemathed: the Kára-Pór-Wood big-line-big-clique conjecture","url":"https://vibemathed.com/problem/big-line-big-clique-four-collinear-or-six-clique","kind":"commentary"},{"label":"arXiv: Cambie, Four collinear points or six visible points","url":"https://arxiv.org/abs/2609.21035","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"big-line-big-clique-four-collinear-or-six-clique","url":"https://vibemathed.com/problem/big-line-big-clique-four-collinear-or-six-clique"},{"registry":"mathdb","id":"315965","title":"Big line big clique conjecture","url":"https://mathdb.com/p/315965/big-line-big-clique-conjecture","note":"Tracks the same Bonnet preprint resolving the (6, 4) case that this entry records."}],"url":"https://whataifound.org/finding/2026-08-19-big-line-big-clique"},{"id":"2026-08-19-caratheodory-umbilic","title":"Counterexample to the smooth Carathéodory conjecture on umbilic points","claim":"An explicit support function gives a smoothly embedded two-sphere bounding a convex body with exactly one umbilic point, so the \\(C^\\infty\\) form of Carathéodory's 1922 conjecture is false.","field":"mathematics","date":"2026-08-19","added":"2026-09-03","lab":"Independent","model":"Claude; Codex","verification":"claimed","autonomy":"ai-assisted","tags":["geometry","differential-geometry","counterexample","lean","construction"],"humans":["Levent Alpöge","John-Paul Smith"],"year_posed":1922,"sources":[{"label":"Levent Alpöge, announcement (X)","url":"https://x.com/__alpoge__/status/2089971359921156203","kind":"announcement"},{"label":"vibemathed: the C-infinity Carathéodory conjecture on umbilic points","url":"https://vibemathed.com/problem/mathbb-c-infty-caratheodory-conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"mathbb-c-infty-caratheodory-conjecture","url":"https://vibemathed.com/problem/mathbb-c-infty-caratheodory-conjecture"}],"url":"https://whataifound.org/finding/2026-08-19-caratheodory-umbilic"},{"id":"2026-08-19-delavina-waller-wiener","title":"The DeLaViña-Waller conjecture on the Wiener index","claim":"Every connected graph on \\(2d+1\\) vertices of diameter \\(d\\) at least 3 is claimed to have Wiener index at most that of the cycle on the same number of vertices, with the equality cases determined.","field":"mathematics","date":"2026-08-19","added":"2026-09-03","lab":"Independent","model":"GPT-5.6 Sol; Claude Fable 5","verification":"author-verified","autonomy":"ai-assisted","tags":["graph-theory","combinatorics","argument"],"humans":["Mingchang Liu"],"year_posed":2008,"sources":[{"label":"Zenodo: the DeLaViña-Waller conjecture on the Wiener index","url":"https://doi.org/10.5281/zenodo.22015517","kind":"research"},{"label":"vibemathed: the DeLaViña-Waller conjecture on the Wiener index","url":"https://vibemathed.com/problem/the-delavina-waller-conjecture-on-the-wiener-index","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"the-delavina-waller-conjecture-on-the-wiener-index","url":"https://vibemathed.com/problem/the-delavina-waller-conjecture-on-the-wiener-index"},{"registry":"mathdb","id":"374919","title":"DeLaViña-Waller conjecture on the Wiener index","url":"https://mathdb.com/p/374919/delavina-waller-conjecture-on-the-wiener-index-of-graphs-of","note":"A background page for the conjecture itself. It does not mention the preprint recorded here and makes no reference to AI involvement, so it establishes the problem's standing in the literature and nothing about this result."}],"url":"https://whataifound.org/finding/2026-08-19-delavina-waller-wiener"},{"id":"2026-08-19-erdos-501-independence","title":"Erdős Problem #501 shown independent of ZFC, with both directions in Lean","claim":"The first question of Erdős Problem #501 is proved independent of ZFC, and both directions are formalized in Lean 4 as statements about the theory ZFC itself.","field":"mathematics","date":"2026-08-19","added":"2026-09-03","lab":"Independent","model":"Sol; Claude","verification":"formal","autonomy":"collaborative","tags":["set-theory","erdos","lean","formalization","forcing"],"humans":["Elliot Glazer"],"year_posed":1961,"sources":[{"label":"GitHub: Erdős Problem #501 in Lean 4","url":"https://github.com/ElliotGlazer/erdos501","kind":"research"},{"label":"Erdős Problems: problem #501","url":"https://www.erdosproblems.com/501","kind":"commentary"},{"label":"vibemathed: Erdős Problem #501, infinite independent sets","url":"https://vibemathed.com/problem/erdos-501-infinite-independent-sets","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"erdos-501-infinite-independent-sets","url":"https://vibemathed.com/problem/erdos-501-infinite-independent-sets"}],"url":"https://whataifound.org/finding/2026-08-19-erdos-501-independence"},{"id":"2026-08-19-kasami-apn-triple-counts","title":"Partial proof of the Kasami APN triple-count conjecture, verified in Lean","claim":"A conjecture from a 2019 cryptography olympiad on triple counts for the Kasami almost perfect nonlinear function is proved in four residue cases and verified exhaustively for small field degrees, with every proof machine-checked.","field":"mathematics","date":"2026-08-19","added":"2026-09-03","lab":"Independent","model":"Claude Fable 5; Harmonic Aristotle","verification":"formal","autonomy":"ai-led","tags":["number-theory","finite-fields","cryptography","lean","formalization"],"humans":["Gábor P. Nagy","Attila Vajda"],"year_posed":2019,"sources":[{"label":"arXiv: on a conjecture on the Kasami APN function","url":"https://arxiv.org/abs/2608.18584","kind":"research"},{"label":"vibemathed: a conjecture on triple counts for the Kasami APN function","url":"https://vibemathed.com/problem/kasami-apn-function-triple-count-conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"kasami-apn-function-triple-count-conjecture","url":"https://vibemathed.com/problem/kasami-apn-function-triple-count-conjecture"},{"registry":"mathdb","id":"383508","title":"Kasami APN function conjecture","url":"https://mathdb.com/p/383508/kasami-apn-function-conjecture"}],"url":"https://whataifound.org/finding/2026-08-19-kasami-apn-triple-counts"},{"id":"2026-08-19-linear-extensions-below-2n","title":"Counting linear extensions below the 2ⁿ barrier","claim":"A deterministic algorithm counts the linear extensions of an arbitrary \\(n\\)-element poset in time \\(O^*(1.89^n)\\), breaking the \\(2^n\\) barrier for the general problem.","field":"computer-science","date":"2026-08-19","added":"2026-09-03","lab":"Independent","model":"Claude Opus 5; ChatGPT 5.6 Sol","verification":"author-verified","autonomy":"ai-led","tags":["algorithms","combinatorics","exact-algorithms"],"humans":["Keigo Oka"],"year_posed":2013,"sources":[{"label":"arXiv: breaking the 2ⁿ barrier for counting linear extensions with a short elementary algorithm","url":"https://arxiv.org/abs/2608.19505","kind":"research"},{"label":"vibemathed: counting linear extensions below the 2ⁿ barrier","url":"https://vibemathed.com/problem/counting-linear-extensions-below-two-to-the-n","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"counting-linear-extensions-below-two-to-the-n","url":"https://vibemathed.com/problem/counting-linear-extensions-below-two-to-the-n"}],"url":"https://whataifound.org/finding/2026-08-19-linear-extensions-below-2n"},{"id":"2026-08-19-yau-tian-donaldson","title":"Counterexample to the Yau–Tian–Donaldson conjecture for constant scalar curvature metrics","claim":"A smooth polarized fivefold that is K-polystable but admits no constant scalar curvature Kähler metric, disproving the form of the Yau–Tian–Donaldson conjecture that Donaldson stated in 2002.","field":"mathematics","date":"2026-08-19","added":"2026-08-21","lab":"Independent","model":"Claude Fable 5, GPT-5.6-sol and Danus","verification":"author-verified","autonomy":"collaborative","tags":["algebraic-geometry","differential-geometry","k-stability","counterexample","construction"],"humans":["Jihao Liu","Bin Dong","Guoxiong Gao"],"year_posed":2002,"sources":[{"label":"arXiv: Disproof of the Yau–Tian–Donaldson conjecture","url":"https://arxiv.org/abs/2608.19301","kind":"research"}],"registrations":[{"registry":"mathdb","id":"383718","title":"Yau–Tian–Donaldson conjecture for constant scalar curvature metrics","url":"https://mathdb.com/p/383718/yau-tian-donaldson-conjecture-for-constant-scalar-curvature","note":"MathDB carries three records for this conjecture under permuted name orders (321390, 331106, 383718). This is the one whose title matches the usual attribution order."}],"url":"https://whataifound.org/finding/2026-08-19-yau-tian-donaldson"},{"id":"2026-08-18-prime-gaps-246","title":"Bounded prime gaps of 246 formalized in Lean from Bombieri-Vinogradov","claim":"A machine-checked Lean development proves that infinitely many pairs of primes differ by at most 246, taking the Bombieri-Vinogradov theorem as a hypothesis rather than proving it.","field":"mathematics","date":"2026-08-18","added":"2026-08-21","lab":"Axiom Math","model":"AxiomProver","verification":"formal","autonomy":"collaborative","tags":["lean","formalization","number-theory","prime-gaps","sieve-methods"],"humans":["Evan Chen","Sidharth Hariharan","Kenny Lau","Bhavik Mehta","Ken Ono","Ashvin Swaminathan","Jesse Thorner","Yunzhou Xie"],"sources":[{"label":"Axiom Math: Lean formalization of bounded gaps between primes","url":"https://primegaps.axiommath.ai/","kind":"research"},{"label":"PrimeGapsLib (Lean 4 source)","url":"https://github.com/AxiomMath/PrimeGapsLib","kind":"research"},{"label":"Axiom announcement (X)","url":"https://x.com/axiommathai/status/2089732764279132449","kind":"announcement"},{"label":"IEEE Spectrum coverage","url":"https://spectrum.ieee.org/axiom-math-246-theorem-formalization","kind":"coverage"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-08-18-000002","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-08-18-000002&version=1","repository":"AxiomMath/PrimeGapsLib","commit":"1faa7b14e82ddebc2772dfb9153922f01b106477","theorems":["bombieriVinogradov_implies_prime_gap_le_246","bombieriVinogradov_implies_nth_prime_gap_le_246"],"checked":"2026-08-18","note":"Registered the day Palomar opened for submissions. The theorem names are where the Bombieri-Vinogradov hypothesis is visible; the project's own page does not carry that qualification."}],"url":"https://whataifound.org/finding/2026-08-18-prime-gaps-246"},{"id":"2026-08-18-stein-riesz-weak-type","title":"Dimension-free weak-type bound for the vector Riesz transform","claim":"The best constant in the weak-type (1,1) bound for the vector Riesz transform on n-dimensional space is at most 2 whatever the dimension, answering a question Stein raised in 1986.","field":"mathematics","date":"2026-08-18","added":"2026-08-31","lab":"Independent","model":"GPT-5.6 Sol and Claude Opus 5.0, with Danus and Rethlas agents","verification":"author-verified","autonomy":"collaborative","tags":["harmonic-analysis","riesz-transforms","argument"],"humans":["Yuyuan Ouyang","Daniel Spector","Cody B. Stockdale"],"year_posed":1986,"sources":[{"label":"arXiv: A dimension-free weak-type (1,1) bound for the vector Riesz transform","url":"https://arxiv.org/abs/2608.18068","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"stein-s-dimension-free-weak-1-1-riesz-transform-problem","url":"https://vibemathed.com/problem/stein-s-dimension-free-weak-1-1-riesz-transform-problem"},{"registry":"mathdb","id":"383291","title":"Stein's vector Riesz transform weak type problem","url":"https://mathdb.com/p/383291/stein-s-vector-riesz-transform-weak-type-problem","note":"Tracks the same problem this entry records a claimed resolution of. As of the September 2026 check the page still carries it as unverified, so it corroborates the problem's standing rather than the result."}],"url":"https://whataifound.org/finding/2026-08-18-stein-riesz-weak-type"},{"id":"2026-08-17-matmul-exponent","title":"Matrix multiplication exponent lowered to below 2.371177","claim":"A reformulated optimization inside the laser method, with AlphaEvolve applied as the final refinement, lowers the best known upper bound on the matrix multiplication exponent from 2.371339 to 2.371177.","field":"computer-science","date":"2026-08-17","added":"2026-08-21","lab":"Google DeepMind","model":"AlphaEvolve","verification":"author-verified","autonomy":"search-scaffold","tags":["alphaevolve","algorithms","matrix-multiplication","complexity","computation"],"humans":["Emilien Dupont","Marvin Eisenberger","Borislav Kozlovskii","Abbas Mehrabian","Francisco J. R. Ruiz","Abigail See","Renfei Zhou","Josh Alman","Virginia Vassilevska Williams","Matej Balog"],"year_posed":1969,"sources":[{"label":"arXiv: Improving the matrix multiplication exponent with modern optimization and AlphaEvolve","url":"https://arxiv.org/abs/2608.16884","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"matrix-multiplication-exponent-2371177","url":"https://vibemathed.com/problem/matrix-multiplication-exponent-2371177"},{"registry":"mathdb","id":"388199","title":"Is the exponent of matrix multiplication 2?","url":"https://mathdb.com/p/388199/is-the-exponent-of-matrix-multiplication-2","note":"Bare problem page for the open question of whether the exponent is 2. It records the problem's standing, not this result: nothing is posted against it."}],"url":"https://whataifound.org/finding/2026-08-17-matmul-exponent"},{"id":"2026-08-16-talagrand-convolution","title":"Talagrand's convolution conjecture proved on the Boolean hypercube","claim":"Convolution by a measure on the Boolean hypercube obeys the dimension-free weak-type decay Talagrand conjectured in 1989, removing the iterated-logarithm factor carried by the best previous bound.","field":"mathematics","date":"2026-08-16","added":"2026-08-21","lab":"Independent","model":"Odin Automatic AI Research Agent","verification":"author-verified","autonomy":"ai-led","tags":["probability","boolean-analysis","concentration","argument"],"humans":["Junwei Lu","Shengtao Guo","Ethan X. Fang"],"year_posed":1989,"sources":[{"label":"arXiv: Weak-Type Bounds for Convolution on the Boolean Hypercube","url":"https://arxiv.org/abs/2608.15515","kind":"research"},{"label":"arXiv: Chen, Talagrand's convolution conjecture up to loglog (prior bound)","url":"https://arxiv.org/abs/2511.19374","kind":"research"},{"label":"arXiv: Shaposhnikov, Some remarks on Talagrand's convolution conjecture","url":"https://arxiv.org/abs/2609.11290","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"talagrand-s-convolution-conjecture","url":"https://vibemathed.com/problem/talagrand-s-convolution-conjecture"},{"registry":"mathdb","id":"371652","title":"Talagrand's convolution conjecture for the Boolean hypercube","url":"https://mathdb.com/p/371652/talagrand-s-convolution-conjecture-for-the-boolean-hypercube"}],"url":"https://whataifound.org/finding/2026-08-16-talagrand-convolution"},{"id":"2026-08-13-banach-isometric","title":"Banach's isometric conjecture settled in the remaining odd dimensions","claim":"A real Banach space whose n-dimensional subspaces are all isometric to one another must be a Hilbert space for every odd n, which together with Gromov's even-dimensional theorem closes a question Banach asked in 1932.","field":"mathematics","date":"2026-08-13","added":"2026-08-21","lab":"Independent","model":"ChatGPT 5.5 Pro, ChatGPT 5.6 Pro and GPT-5.6 Sol","verification":"author-verified","autonomy":"ai-assisted","tags":["functional-analysis","banach-spaces","argument","geometry"],"humans":["Xinbao Lu","Kaiwen Yang"],"year_posed":1932,"sources":[{"label":"arXiv: A solution to Banach's isometric conjecture","url":"https://arxiv.org/abs/2608.13536","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"banach-s-isometric-conjecture","url":"https://vibemathed.com/problem/banach-s-isometric-conjecture"},{"registry":"mathdb","id":"383555","title":"Banach's isometric conjecture","url":"https://mathdb.com/p/383555/banach-s-isometric-conjecture"}],"url":"https://whataifound.org/finding/2026-08-13-banach-isometric"},{"id":"2026-08-13-sop2-sop3","title":"SOP₂ and SOP₃ theories shown to coincide","claim":"The classes of \\(\\mathrm{SOP}_2\\) and \\(\\mathrm{SOP}_3\\) first-order theories are the same, answering a 2004 question of Džamonja and Shelah and collapsing the bottom of the SOP hierarchy to a single class.","field":"mathematics","date":"2026-08-13","added":"2026-08-14","lab":"Independent","model":"ChatGPT 5.6","verification":"author-verified","autonomy":"collaborative","tags":["model-theory","logic","classification-theory"],"humans":["Artem Chernikov"],"year_posed":2004,"sources":[{"label":"arXiv: SOP₂ = SOP₃","url":"https://arxiv.org/abs/2608.13291","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"sop-2-sop-3","url":"https://vibemathed.com/problem/sop-2-sop-3"}],"url":"https://whataifound.org/finding/2026-08-13-sop2-sop3"},{"id":"2026-08-12-liquid-drop-minimizers","title":"Complete minimizer picture for Gamow's liquid drop model","claim":"Balls uniquely minimize the Gamow liquid drop energy at every volume up to a sharp threshold of about 3.51, and above that threshold no minimizer exists, closing a gap that partial results had narrowed from both sides without meeting.","field":"mathematics","date":"2026-08-12","added":"2026-08-14","lab":"Independent","model":"ChatGPT 5.6 Pro","verification":"author-verified","autonomy":"ai-led","tags":["calculus-of-variations","geometric-analysis","mathematical-physics"],"humans":["Otis Chodosh","Matilde Gianocca"],"sources":[{"label":"arXiv: No compromise in the liquid drop model","url":"https://arxiv.org/abs/2608.11517","kind":"research"},{"label":"arXiv: An improved nonexistence bound for the liquid drop model","url":"https://arxiv.org/abs/2608.09000","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"gamow-liquid-drop-minimizer-conjecture","url":"https://vibemathed.com/problem/gamow-liquid-drop-minimizer-conjecture"},{"registry":"mathdb","id":"355211","title":"Liquid-drop minimizer conjecture","url":"https://mathdb.com/p/355211/liquid-drop-minimizer-conjecture"}],"url":"https://whataifound.org/finding/2026-08-12-liquid-drop-minimizers"},{"id":"2026-08-11-prescribed-cycle-recovery","title":"A prescribed Hamiltonian cycle that a book-embedding algorithm cannot produce","claim":"A 16-vertex graph carries a Hamiltonian cycle that the Alam et al. book-embedding algorithm cannot return for any choice of dual spanning tree, answering a question of Bekos, Kaufmann and Pfister in the negative.","field":"computer-science","date":"2026-08-11","added":"2026-08-25","lab":"Independent","model":"OpenAI Codex, with Claude for adversarial review","verification":"formal","autonomy":"ai-assisted","tags":["lean","formalization","graph-theory","book-embedding","algorithms","construction"],"humans":["Lennart Rudolph"],"sources":[{"label":"Zenodo: A Counterexample to Prescribed-Cycle Recovery in Barnette Graphs","url":"https://zenodo.org/records/21890733","kind":"research"},{"label":"Lean development: lennrt/palomar-formalizations","url":"https://github.com/lennrt/palomar-formalizations","kind":"research"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-08-21-000002","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-08-21-000002&version=1","repository":"lennrt/palomar-formalizations","commit":"090b3b300ba8ec76fdba09a17f086953d13f2653","theorems":["BarnettePalomar.concrete_graph_certificate","BarnettePalomar.face_coloring_certificate","BarnettePalomar.property_one_excludes_prescribed_cycle"],"checked":"2026-08-21","note":"Covers the finite core only. The sphere embedding and the algorithm's Property 1 are external inputs, which the record states."}],"url":"https://whataifound.org/finding/2026-08-11-prescribed-cycle-recovery"},{"id":"2026-08-10-zeta-zeros-critical-line","title":"Proportion of zeta zeros on the critical line raised to 67.25%","claim":"An unconditional proof that at least 67.25% of the nontrivial zeros of the Riemann zeta function are simple and lie on the critical line, up from a previous record of about 41.6%, with a machine-checked Lean formalization.","field":"mathematics","date":"2026-08-10","added":"2026-08-11","lab":"Anthropic","model":"Claude (unreleased research version)","verification":"formal","autonomy":"ai-led","tags":["lean","number-theory","riemann-hypothesis","multi-agent"],"humans":["Jarred Sumner","Levent Alpöge","Ralph Furman","Eric Easley"],"sources":[{"label":"Anthropic: paper (PDF)","url":"https://www-cdn.anthropic.com/564f962e60643842f5fcb4a17c9dbc8f608f1c37.pdf","kind":"research"},{"label":"Lean 4 formalization (anthropics/zeta-23-lean)","url":"https://github.com/anthropics/zeta-23-lean","kind":"research"},{"label":"Session transcript (PDF)","url":"https://www-cdn.anthropic.com/8a0d1add3c637b858a9a181e98c40e9548c3f44f.pdf","kind":"announcement"},{"label":"arXiv: Lamzouri, A new proof that more than 2/3 of the zeros of the Riemann zeta function are simple and on the critical line","url":"https://arxiv.org/abs/2609.02882","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"more-than-67-of-riemann-zeta-zeros-are-on-the-critical-line","url":"https://vibemathed.com/problem/more-than-67-of-riemann-zeta-zeros-are-on-the-critical-line","title":"The Proportion of Zeta Zeros on the Critical Line"}],"url":"https://whataifound.org/finding/2026-08-10-zeta-zeros-critical-line"},{"id":"2026-08-08-petersen-coloring","title":"A 112-vertex counterexample to the Petersen coloring conjecture","claim":"An explicit simple bridgeless cubic graph on 112 vertices admits no Petersen coloring, and hence no normal 5-edge-coloring, refuting a conjecture of Jaeger from 1985 with machine-checked UNSAT certificates.","field":"mathematics","date":"2026-08-08","added":"2026-08-14","lab":"Independent","model":"Unnamed OpenAI model","verification":"formal","autonomy":"ai-assisted","tags":["graph-theory","counterexample","sat-solver","combinatorics"],"humans":["Bryce Putman"],"year_posed":1985,"sources":[{"label":"arXiv: A 112-Vertex Counterexample to the Petersen Coloring Conjecture","url":"https://arxiv.org/abs/2608.10012","kind":"research"},{"label":"Zenodo: reproducibility artifacts and checked DRAT certificates","url":"https://doi.org/10.5281/zenodo.21845291","kind":"research"},{"label":"Open Problem Garden: Petersen coloring conjecture","url":"https://www.openproblemgarden.org/op/petersen_coloring_conjecture","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"petersen-coloring-conjecture","url":"https://vibemathed.com/problem/petersen-coloring-conjecture"},{"registry":"mathdb","id":"316003","title":"Petersen coloring conjecture","url":"https://mathdb.com/p/316003/petersen-coloring-conjecture"}],"url":"https://whataifound.org/finding/2026-08-08-petersen-coloring"},{"id":"2026-08-06-kreiss-constant-separation","title":"Separation between the ordinary and strong Kreiss constants","claim":"A negative solution to the inverse generator problem on Hilbert spaces yields an operator whose Cayley transforms satisfy the ordinary Kreiss condition but are neither strongly Kreiss bounded nor power bounded.","field":"mathematics","date":"2026-08-06","added":"2026-09-03","lab":"Independent","model":"ChatGPT 5.6 Pro; Claude Fable","verification":"author-verified","autonomy":"ai-assisted","tags":["analysis","operator-theory","counterexample","lean"],"humans":["Emiel Lorist","Martin Meyries","Mark Veraar"],"year_posed":2025,"sources":[{"label":"arXiv: a solution to the inverse generator problem and related questions","url":"https://arxiv.org/abs/2608.06272","kind":"research"},{"label":"GitHub: Lean 4 formalization of Theorem 1.1","url":"https://github.com/zoowirt/inverse-generator-lean","kind":"research"},{"label":"vibemathed: separation between the ordinary and strong Kreiss constants","url":"https://vibemathed.com/problem/separation-of-ordinary-and-strong-kreiss-constants","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"separation-of-ordinary-and-strong-kreiss-constants","url":"https://vibemathed.com/problem/separation-of-ordinary-and-strong-kreiss-constants"}],"url":"https://whataifound.org/finding/2026-08-06-kreiss-constant-separation"},{"id":"2026-08-05-schiffer-conjecture","title":"Counterexamples to Schiffer's conjecture and the Pompeiu problem","claim":"Infinitely many planar domains that are not balls admit a Neumann eigenfunction of the Laplacian that is constant on the boundary, disproving Schiffer's conjecture and, through a classical equivalence, the 1929 Pompeiu problem.","field":"mathematics","date":"2026-08-05","added":"2026-08-14","lab":"Independent","model":"GPT-5.6, Claude Opus 4.8, Claude Fable 5","verification":"formal","autonomy":"ai-assisted","tags":["lean","spectral-geometry","counterexample","analysis"],"humans":["Gonzalo Cao-Labora","Jaume de Dios Pont"],"year_posed":1929,"sources":[{"label":"arXiv: Counterexamples to Schiffer's Conjecture","url":"https://arxiv.org/abs/2608.05114","kind":"research"},{"label":"Lean 4 formalization (jaumededios/Schiffer)","url":"https://github.com/jaumededios/Schiffer","kind":"research"},{"label":"Wikipedia: Pompeiu problem","url":"https://en.wikipedia.org/wiki/Pompeiu_problem","kind":"commentary"},{"label":"arXiv: Colbrook and Stepaniants, A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures","url":"https://arxiv.org/abs/2608.01579","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"schiffer-conjecture","url":"https://vibemathed.com/problem/schiffer-conjecture"},{"registry":"mathdb","id":"315903","title":"Pompeiu problem","url":"https://mathdb.com/p/315903/pompeiu-problem"}],"url":"https://whataifound.org/finding/2026-08-05-schiffer-conjecture"},{"id":"2026-08-05-sendov-conjecture","title":"Sendov's conjecture proved for every degree","claim":"For every complex polynomial of degree at least two whose zeros all lie in the closed unit disk, each zero has a critical point of the polynomial within distance one, closing a question open since 1959.","field":"mathematics","date":"2026-08-05","added":"2026-08-14","lab":"Independent","model":"GPT-5.6 Pro","verification":"formal","autonomy":"collaborative","tags":["lean","complex-analysis","polynomials","formalization"],"humans":["Lech Mazur"],"year_posed":1959,"sources":[{"label":"ProofAtlas: A Computer-Assisted Proof of Sendov's Conjecture (PDF)","url":"https://www.proofatlas.ai/papers/sendov-conjecture/SENDOV_CONJECTURE_PROOF_AUGUST_5_2026.pdf","kind":"research"},{"label":"Terence Tao: A digestion of the proof of Sendov's conjecture","url":"https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/","kind":"commentary"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-08-13-000001","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-08-13-000001&version=1","repository":"teorth/sendov","commit":"e356ef6d706cc8687369f3b21bb009587e88cbe9","theorems":["SendovConjecture.sendov","SendovConjecture.phelps_rodriguez"],"checked":"2026-08-13","note":"Permitted axioms are exactly propext, Quot.sound and Classical.choice, so the development adds none of its own. This is the artifact the formal grade already rested on, now checked by someone other than its author."},{"registry":"vibemathed","id":"sendov-s-conjecture","url":"https://vibemathed.com/problem/sendov-s-conjecture"},{"registry":"mathdb","id":"315904","title":"Sendov's conjecture","url":"https://mathdb.com/p/315904/sendov-s-conjecture"},{"registry":"proofatlas","id":"sendov-conjecture","url":"https://proofatlas.ai/formalizations/sendov-conjecture/","title":"Sendov's conjecture","note":"ProofAtlas records that the build passed with no unfinished proof steps, and that the record has not reached its accepted-result status, which needs four independent reviews. Its recorded build is not the same claim as the published bundle being rebuildable; this entry's caveat that the distributed package ships no lakefile or manifest still stands."}],"url":"https://whataifound.org/finding/2026-08-05-sendov-conjecture"},{"id":"2026-08-04-moore-bound","title":"Asymptotic degree-diameter problem resolved for fixed diameter","claim":"The maximum order of a graph with maximum degree \\(d\\) and diameter \\(k\\) satisfies \\(n_k(d)/d^k\\) tending to 1 as \\(d\\) grows, for every fixed \\(k\\), resolving the asymptotic form of a question open since 1978, with a Lean 4 formalization.","field":"mathematics","date":"2026-08-04","added":"2026-08-11","lab":"Independent","model":"GPT-5.6 Pro","verification":"formal","autonomy":"ai-assisted","tags":["lean","graph-theory","combinatorics","extremal-combinatorics"],"humans":["Wouter Cames van Batenburg","Samuel Korsky"],"year_posed":1978,"sources":[{"label":"arXiv: Asymptotically attaining the Moore bound","url":"https://arxiv.org/abs/2608.03965","kind":"research"},{"label":"Lean 4 formalization (woutercvb/wewantmoore)","url":"https://github.com/woutercvb/wewantmoore","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"asymptotically-attaining-the-moore-bound","url":"https://vibemathed.com/problem/asymptotically-attaining-the-moore-bound","title":"Asymptotically attaining the Moore bound"},{"registry":"mathdb","id":"316015","title":"Degree diameter problem","url":"https://mathdb.com/p/316015/degree-diameter-problem"}],"url":"https://whataifound.org/finding/2026-08-04-moore-bound"},{"id":"2026-08-01-astra-ten-advances","title":"Ten results in mathematics and theoretical computer science with Lean certificates","claim":"An unreleased OpenAI model produced ten results including the first explicit non-sofic group and a disproof of Connes's rigidity conjecture, each published with a machine-checkable Lean 4 proof.","field":"mathematics","date":"2026-08-01","added":"2026-08-06","lab":"OpenAI","model":"Astra","verification":"formal","autonomy":"ai-led","tags":["group-theory","lean","formalization","sphere-packing","quantum-complexity"],"year_posed":1999,"sources":[{"label":"Lean 4 certificates for all ten results","url":"https://github.com/openai/ten-proofs","kind":"research"},{"label":"OpenAI: Ten advances in mathematics and theoretical computer science","url":"https://openai.com/index/ten-advances-in-mathematics/","kind":"announcement"},{"label":"Andreas Thom on the non-sofic-group result, guest post on Terence Tao's blog","url":"https://terrytao.wordpress.com/2026/09/11/on-the-existence-of-non-sofic-groups/","kind":"challenge"},{"label":"arXiv: Zhou, ICC property (T) groups without W*-superrigidity","url":"https://arxiv.org/abs/2608.02327","kind":"commentary"},{"label":"arXiv: Kun and Thom, Nonsofic wreath products of residually finite groups","url":"https://arxiv.org/abs/2608.06222","kind":"commentary"},{"label":"arXiv: Fournier-Facio, A torsion-free non-sofic group","url":"https://arxiv.org/abs/2608.02025","kind":"commentary"},{"label":"arXiv: Sienicki and Sienicki, A human audit of OpenAI's AI-generated mathematical proofs","url":"https://arxiv.org/abs/2608.14673","kind":"commentary"}],"url":"https://whataifound.org/finding/2026-08-01-astra-ten-advances"},{"id":"2026-07-29-sumset-difference-exponent","title":"Optimal exponent relating sumsets and difference sets determined","claim":"The least universal exponent \\(c\\) with \\(|A+A|/|A|\\) bounded by \\((|A-A|/|A|)^c\\) for every finite integer set \\(A\\) is determined, settling the extremal question with a Lean 4 formalization.","field":"mathematics","date":"2026-07-29","added":"2026-08-11","lab":"Tencent Hunyuan","model":"Hy3 (Hyra research agent)","verification":"formal","autonomy":"ai-led","tags":["lean","additive-combinatorics","number-theory"],"humans":["Haowei Lin","Shanda Li"],"sources":[{"label":"arXiv: Settling the Optimal Exponent Relating Sumsets and Difference Sets","url":"https://arxiv.org/abs/2607.27199","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"optimal-exponent-relating-sumsets-and-difference-sets","url":"https://vibemathed.com/problem/optimal-exponent-relating-sumsets-and-difference-sets","title":"Optimal Exponent Relating Sumsets and Difference Sets"},{"registry":"mathdb","id":"315713","title":"Optimal exponent relating sumsets and difference sets","url":"https://mathdb.com/p/315713/optimal-exponent-relating-sumsets-and-difference-sets"}],"url":"https://whataifound.org/finding/2026-07-29-sumset-difference-exponent"},{"id":"2026-07-28-kemeny-three-voters","title":"Kemeny rank aggregation shown NP-hard for three voters","claim":"Computing a Kemeny-optimal aggregate ranking is NP-hard when the input is exactly three complete rankings, closing the minimal open case left by hardness results for even voter counts.","field":"computer-science","date":"2026-07-28","added":"2026-08-11","lab":"Independent","model":"GPT-5.6 Sol Ultra, Claude Fable 5","verification":"formal","autonomy":"ai-led","tags":["lean","complexity-theory","computational-social-choice"],"humans":["Dominik Peters"],"year_posed":2001,"sources":[{"label":"arXiv: Kemeny Rank Aggregation is NP-Hard for Three Voters","url":"https://arxiv.org/abs/2607.25540","kind":"research"},{"label":"arXiv: Madarasi, The complexity of Kemeny aggregation with three rankings","url":"https://arxiv.org/abs/2607.28588","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"kemeny-three-voters","url":"https://vibemathed.com/problem/kemeny-three-voters","title":"Kemeny Rank Aggregation for Three Voters"},{"registry":"mathdb","id":"315674","title":"Kemeny rank aggregation for three voters","url":"https://mathdb.com/p/315674/kemeny-rank-aggregation-for-three-voters"}],"url":"https://whataifound.org/finding/2026-07-28-kemeny-three-voters"},{"id":"2026-07-27-feige-conjecture","title":"Feige's conjecture on sums of nonnegative random variables settled","claim":"For independent nonnegative random variables with mean at most 1 and sum S, the probability that S is below its mean plus one is at least 1/e, the sharp constant Feige conjectured in 2004; three independent proofs appeared within days.","field":"mathematics","date":"2026-07-27","added":"2026-08-11","lab":"Independent","model":"ChatGPT 5.6 Pro","verification":"formal","autonomy":"ai-led","tags":["lean","probability","concentration-inequalities"],"humans":["Weibo Fu","Yanjun Han","Guanyang Wang","Jun Yan","Peng Zhang","Zhengqing Zhou"],"year_posed":2004,"sources":[{"label":"arXiv: Sharp small-deviation inequalities for sums of independent nonnegative random variables","url":"https://arxiv.org/abs/2607.23980","kind":"research"},{"label":"Lean formalization (pengzhang91/Feige)","url":"https://github.com/pengzhang91/Feige","kind":"research"},{"label":"arXiv: On Feige's conjecture (Nie and Wei)","url":"https://arxiv.org/abs/2607.24528","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"feiges-conjecture","url":"https://vibemathed.com/problem/feiges-conjecture","title":"Feige's Conjecture"},{"registry":"mathdb","id":"315661","title":"Feige's 1/e conjecture","url":"https://mathdb.com/p/315661/feige-s-1-e-conjecture"}],"url":"https://whataifound.org/finding/2026-07-27-feige-conjecture"},{"id":"2026-07-22-dinitz-garg-goemans","title":"Counterexample to the Dinitz–Garg–Goemans conjecture","claim":"An explicit seven-node network whose cheapest single-route (unsplittable) shipping costs more than its fractional cost even under the allowed capacity slack, disproving a conjecture from the late 1990s.","field":"computer-science","date":"2026-07-22","added":"2026-07-24","lab":"Independent","model":"GPT-5.6 Pro","verification":"formal","autonomy":"ai-led","tags":["combinatorial-optimization","network-flow","counterexample","unsplittable-flow"],"humans":["Dmitry Rybin"],"year_posed":1999,"sources":[{"label":"Dmitry Rybin announcement (X)","url":"https://x.com/DmitryRybin1/status/2079907499545919968","kind":"announcement"},{"label":"Coverage: officechai","url":"https://officechai.com/ai/mathematician-says-gpt-5-6-disproved-the-30-year-old-dinitz-garg-goemans-conjecture-with-4-simple-prompts/","kind":"coverage"},{"label":"Archive of Formal Proofs: a formal counterexample to the cost-preserving single-source unsplittable flow conjecture","url":"https://isa-afp.org/entries/Dinitz_Garg_Goemans_Counterexample.html","kind":"research"}],"registrations":[{"registry":"mathdb","id":"316187","title":"Dinitz–Garg–Goemans conjecture","url":"https://mathdb.com/p/316187/dinitz-garg-goemans-conjecture"},{"registry":"vibemathed","id":"dinitz-garg-goemans-unsplittable-flow","url":"https://vibemathed.com/problem/dinitz-garg-goemans-unsplittable-flow"}],"url":"https://whataifound.org/finding/2026-07-22-dinitz-garg-goemans"},{"id":"2026-07-20-gaussian-moments","title":"Counterexamples to the Gaussian moments conjecture","claim":"Explicit low-degree polynomials disproving a 2017 conjecture that had been proposed as a route to proving the Jacobian conjecture, found days after that conjecture was itself disproved.","field":"mathematics","date":"2026-07-20","added":"2026-07-27","lab":"Independent","model":"GPT-5.6 Sol Pro + Claude Fable 5","verification":"author-verified","autonomy":"ai-led","tags":["algebra","polynomial-maps","counterexample","jacobian-conjecture"],"humans":["Christopher D. Long"],"year_posed":2017,"sources":[{"label":"arXiv: Small Counterexamples to the Gaussian Moments Conjecture","url":"https://arxiv.org/abs/2607.18186","kind":"research"},{"label":"Derksen, van den Essen, Zhao: The Gaussian Moments Conjecture and the Jacobian Conjecture","url":"https://arxiv.org/abs/1506.05192","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"gaussian-moments-conjecture","url":"https://vibemathed.com/problem/gaussian-moments-conjecture"}],"url":"https://whataifound.org/finding/2026-07-20-gaussian-moments"},{"id":"2026-07-20-gaussian-product-inequality","title":"Gaussian product inequality conjecture proved","claim":"For any centered Gaussian vector and positive exponents, the expectation of the product of absolute powers is at least the product of the individual expectations, settling a conjecture posed in 2007.","field":"mathematics","date":"2026-07-20","added":"2026-08-11","lab":"Independent","model":"ChatGPT 5.6 Sol","verification":"formal","autonomy":"ai-led","tags":["lean","probability","gaussian-inequalities"],"humans":["Frédéric Ouimet","Dylan Greaves"],"year_posed":2007,"sources":[{"label":"A proof of the strong Gaussian product inequality conjecture","url":"https://doi.org/10.13140/RG.2.2.17569.77923/1","kind":"research"},{"label":"Lean formalization (dylgre/gaussian-product-inequality)","url":"https://github.com/dylgre/gaussian-product-inequality","kind":"research"},{"label":"Public chat transcript","url":"https://chatgpt.com/share/6a5ea69b-1648-83e8-80b1-014ae0b1003c","kind":"announcement"}],"registrations":[{"registry":"vibemathed","id":"gaussian-product-inequality-conjecture","url":"https://vibemathed.com/problem/gaussian-product-inequality-conjecture","title":"Gaussian product inequality conjecture"},{"registry":"mathdb","id":"330065","title":"The Gaussian Product Conjecture","url":"https://mathdb.com/p/330065/the-gaussian-product-conjecture"}],"url":"https://whataifound.org/finding/2026-07-20-gaussian-product-inequality"},{"id":"2026-07-20-kourovka-notebook","title":"Eight problems from the Kourovka Notebook solved and formalized in Lean","claim":"A formal reasoning agent developed the proof strategies for eight open problems in group theory without human guidance on which mathematical steps to take, and machine-checked every one in Lean 4.","field":"mathematics","date":"2026-07-20","added":"2026-08-06","lab":"Harmonic","model":"Aristotle","verification":"formal","autonomy":"autonomous","tags":["group-theory","lean","formalization","kourovka-notebook","autonomous-discovery"],"humans":["Wouter van Doorn","Elias Judin","Pietro Monticone","Daniel Morrison"],"year_posed":1969,"sources":[{"label":"arXiv: On Some Problems from the Kourovka Notebook","url":"https://arxiv.org/abs/2607.17477","kind":"research"},{"label":"Lean 4 formalizations of all eight solutions","url":"https://github.com/pitmonticone/Kourovka","kind":"research"}],"url":"https://whataifound.org/finding/2026-07-20-kourovka-notebook"},{"id":"2026-07-19-jacobian-conjecture","title":"Counterexample to the Jacobian conjecture in dimension three","claim":"An explicit polynomial map in three variables with constant Jacobian determinant \\(-2\\) that is nevertheless not invertible, disproving a conjecture open since 1939.","field":"mathematics","date":"2026-07-19","added":"2026-07-20","lab":"Anthropic","model":"Claude Fable 5","verification":"formal","autonomy":"collaborative","tags":["algebraic-geometry","counterexample","polynomial-maps"],"humans":["Levent Alpöge"],"year_posed":1939,"sources":[{"label":"The Jacobian counterexample, explained","url":"https://jacobianfun.org/jacobian-explained","kind":"research"},{"label":"Ulam: A counterexample to the Jacobian conjecture (PDF), the seven-page algebraic verification of the announced map","url":"https://www.ulam.ai/research/jacobian.pdf","kind":"research"},{"label":"Alexis Gallagher: Jacobian Conjecture Disproved!","url":"https://alexisgallagher.com/posts/2026/jacobianfun/","kind":"commentary"},{"label":"Hacker News discussion","url":"https://news.ycombinator.com/item?id=48973869","kind":"commentary"},{"label":"Borisov, Gabber and Vasiu: on endomorphisms of affine spaces and the Jacobian problem, whose supplemental statement on page 160 raises priority and disclosure questions","url":"https://arxiv.org/abs/2609.05746","kind":"challenge"}],"registrations":[{"registry":"mathdb","id":"315779","title":"Jacobian conjecture","url":"https://mathdb.com/p/315779/jacobian-conjecture"},{"registry":"vibemathed","id":"jacobian-conjecture","url":"https://vibemathed.com/problem/jacobian-conjecture"},{"registry":"palomar","id":"PALOMAR-2026-08-21-000006","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-08-21-000006&version=1","repository":"Paul-Lez/jacobian-conjecture","commit":"b244ea482ed086297e379d73e6724cd26b2d301f","theorems":["JacobianConjecture.jacobian_conjecture"],"checked":"2026-08-21","note":"A Comparator wrapper of the formalization by Paul Lezeau and Dean Cureton in Google DeepMind's formal-conjectures, whose Lean source names the construction as Alpöge and Fable's counterexample. It records a stronger statement than this entry claims, disproving the generalized conjecture over every nontrivial commutative ring rather than in characteristic zero alone, and omits the two-variable case, which stays open."},{"registry":"palomar","id":"PALOMAR-2026-08-27-000013","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-08-27-000013&version=1","repository":"Arthur742Ramos/jacobian-conjecture-lean","commit":"8db55ea3ffa8ba90094d6ef78ee3351ddfce01ca","theorems":["JacobianCounterexample.jacobianDet_F","JacobianCounterexample.explicit_three_point_fibre","JacobianCounterexample.not_jacobian_conjecture_complex"],"checked":"2026-08-27","note":"A second and independent Lean formalization of the same map, by Ramos, Hulak and de Queiroz, sharing no code with the Lezeau and Cureton development already cited. It records the two-variable case as untouched, as this entry does."}],"url":"https://whataifound.org/finding/2026-07-19-jacobian-conjecture"},{"id":"2026-07-14-sabidussi-compatibility","title":"Sabidussi's compatibility conjecture proved","claim":"The edges of a finite connected multigraph carrying a closed eulerian trail can be partitioned into circuits so that no circuit contains two edges used consecutively in the trail, with a Lean 4 formalization.","field":"mathematics","date":"2026-07-14","added":"2026-08-11","lab":"Independent","model":"GPT-5.6 Pro, GPT-5.6 Sol","verification":"formal","autonomy":"collaborative","tags":["lean","graph-theory","combinatorics"],"humans":["Nikolay Ulyanov"],"sources":[{"label":"arXiv: Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture","url":"https://arxiv.org/abs/2607.13225","kind":"research"},{"label":"Lean 4 formalization (gexahedron/sabidussi-lean)","url":"https://github.com/gexahedron/sabidussi-lean","kind":"research"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-08-17-000003","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-08-17-000003&version=1","repository":"gexahedron/sabidussi-lean","commit":"58307d74da99ec6e4fe28e012c30c83e369c54c3","theorems":["sabidussi_compatibility_ordinary"],"checked":"2026-08-17","note":"Palomar's record does not restate the theorem in prose, so what the registration certifies is that formal statement rather than the preprint's phrasing of it."},{"registry":"vibemathed","id":"sabidussi-compatibility","url":"https://vibemathed.com/problem/sabidussi-compatibility","title":"Sabidussi's Compatibility Conjecture"},{"registry":"mathdb","id":"388102","title":"Sabidussi's compatibility conjecture","url":"https://mathdb.com/p/388102/sabidussi-s-compatibility-conjecture","note":"A bare problem record: MathDB has no progress summary and no solution posted for it, so this places the problem in that catalogue rather than corroborating the resolution."}],"url":"https://whataifound.org/finding/2026-07-14-sabidussi-compatibility"},{"id":"2026-07-14-zeroth-order-oracle-bound","title":"Near-quadratic lower bound for derivative-free convex optimization","claim":"A lower bound of order \\(d^2/\\log d\\) on the number of exact function evaluations needed to minimize a convex Lipschitz function, closing a gap open since 1996 and showing a 1996 algorithm was essentially optimal.","field":"mathematics","date":"2026-07-14","added":"2026-07-27","lab":"Independent","model":"GPT-5.6 Sol Pro","verification":"formal","autonomy":"ai-led","tags":["optimization","complexity-theory","lower-bounds","lean"],"humans":["Phillip Kerger"],"year_posed":1996,"sources":[{"label":"arXiv: Closing the Oracle-Complexity Gap in Derivative-Free Convex Optimization","url":"https://arxiv.org/abs/2607.13335","kind":"research"},{"label":"Lean verification, prompt and chat logs","url":"https://github.com/PhillipKerger/zero-order-bounds-lean-verification","kind":"research"}],"url":"https://whataifound.org/finding/2026-07-14-zeroth-order-oracle-bound"},{"id":"2026-07-11-grothendieck-group-schemes","title":"Counterexample to Grothendieck's question on finite flat group schemes","claim":"A finite locally free group scheme of order four whose fourth power map is not trivial, answering a question Grothendieck raised in the 1960s; one model produced the construction and another formalised it in Lean.","field":"mathematics","date":"2026-07-11","added":"2026-07-29","lab":"Independent","model":"OpenAI Sol (construction); Claude Fable (Lean formalisation)","verification":"formal","autonomy":"collaborative","tags":["algebraic-geometry","group-schemes","counterexample","lean","formalization"],"humans":["Akhil Mathew","Kevin Buzzard"],"sources":[{"label":"Kevin Buzzard: Human mathematicians are being outcounterexampled","url":"https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/","kind":"announcement"},{"label":"mathlib4 PR #41748: a finite free group scheme of order four not killed by four","url":"https://github.com/leanprover-community/mathlib4/pull/41748","kind":"research"}],"registrations":[{"registry":"mathdb","id":"315784","title":"Grothendieck's group-scheme question","url":"https://mathdb.com/p/315784/grothendieck-s-group-scheme-question"},{"registry":"vibemathed","id":"grothendieck-finite-flat-group-schemes","url":"https://vibemathed.com/problem/grothendieck-finite-flat-group-schemes"}],"url":"https://whataifound.org/finding/2026-07-11-grothendieck-group-schemes"},{"id":"2026-07-10-cycle-double-cover","title":"Cycle double cover conjecture proved for all bridgeless multigraphs","claim":"Every finite bridgeless loopless multigraph has a multiset of cycles covering each edge exactly twice, resolving a conjecture open since 1973, with a machine-checked Lean proof of the unconditional statement.","field":"mathematics","date":"2026-07-10","added":"2026-08-14","lab":"OpenAI","model":"GPT-5.6 Sol Ultra","verification":"formal","autonomy":"ai-led","tags":["lean","graph-theory","combinatorics","multi-agent"],"year_posed":1973,"sources":[{"label":"OpenAI: A proof of the cycle double cover conjecture (PDF)","url":"https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf","kind":"research"},{"label":"Lean 4 formalization (openai/cdc-lean)","url":"https://github.com/openai/cdc-lean","kind":"research"},{"label":"OpenAI: the prompt used for the proof (PDF)","url":"https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf","kind":"announcement"},{"label":"Ethan Knight announcement (X)","url":"https://x.com/__eknight__/status/2075643450196971805","kind":"announcement"},{"label":"arXiv: A proof of the cycle double cover conjecture by OpenAI: An exposition","url":"https://arxiv.org/abs/2607.16356","kind":"commentary"},{"label":"arXiv: Three-Bit Flows and Cycle Covers. Part I","url":"https://arxiv.org/abs/2607.14140","kind":"commentary"},{"label":"Scientific American: ChatGPT just proved another 50-year-old math conjecture","url":"https://www.scientificamerican.com/article/chatgpt-just-proved-another-50-year-old-math-conjecture/","kind":"coverage"},{"label":"arXiv: Geelen, OpenAI's proof of the Cycle Double Cover Theorem","url":"https://arxiv.org/abs/2607.15399","kind":"commentary"}],"registrations":[{"registry":"vibemathed","id":"cycle-double-cover-conjecture","url":"https://vibemathed.com/problem/cycle-double-cover-conjecture"},{"registry":"mathdb","id":"316019","title":"Cycle double cover conjecture","url":"https://mathdb.com/p/316019/cycle-double-cover-conjecture"}],"url":"https://whataifound.org/finding/2026-07-10-cycle-double-cover"},{"id":"2026-06-25-herculaneum-scroll-read","title":"First Herculaneum scroll read end to end without unrolling it","claim":"PHerc. 1667 was virtually unwrapped and read in full from X-ray scans using learned ink detection: about 1.4 metres of papyrus across roughly 22 columns of Greek, identified as Philodemus, On Gods, Book 8.","field":"archaeology","date":"2026-06-25","added":"2026-07-29","lab":"Vesuvius Challenge","model":"Community-developed ink-detection neural networks","verification":"author-verified","autonomy":"ai-assisted","tags":["papyrology","virtual-unwrapping","ink-detection","ancient-texts"],"humans":["Brent Seales","Luke Farritor","Youssef Nader","Julian Schilliger"],"sources":[{"label":"Complete virtual unwrapping and reading of a rolled Herculaneum papyrus","url":"https://arxiv.org/abs/2606.29085","kind":"research"},{"label":"Vesuvius Challenge: An entire Herculaneum scroll has been read for the first time","url":"https://scrollprize.org/firstscroll","kind":"announcement"},{"label":"Vesuvius Challenge","url":"https://scrollprize.org/","kind":"announcement"}],"url":"https://whataifound.org/finding/2026-06-25-herculaneum-scroll-read"},{"id":"2026-06-17-kagome-superconductors","title":"Two kagome superconductors predicted by machine learning and confirmed in the lab","claim":"A screening pipeline that narrowed over 1.3 million candidate structures picked out YRu3B2 and LuRu3B2, which were then synthesized and measured to superconduct at 0.81 K and 0.95 K.","field":"materials","date":"2026-06-17","added":"2026-08-06","lab":"Aalto University / Rice University","model":"Unknown","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["superconductivity","kagome","high-throughput-screening","dft","experimental-confirmation"],"humans":["Rose Albu Mustaf","Päivi Törmä","Emilia Morosan","B. Andrei Bernevig","Miguel A. L. Marques"],"sources":[{"label":"arXiv: Machine Learning-Guided Discovery of Kagome Superconductors YRu3B2 and LuRu3B2","url":"https://arxiv.org/abs/2512.16945","kind":"research"},{"label":"ScienceDaily: AI just supercharged the race to find room temperature superconductors","url":"https://www.sciencedaily.com/releases/2026/07/260701205006.htm","kind":"coverage"}],"url":"https://whataifound.org/finding/2026-06-17-kagome-superconductors"},{"id":"2026-06-02-jamming-exponent-identity","title":"Identity for the critical exponents of jamming derived analytically","claim":"The relation \\(a + b = 1\\) between critical exponents at the jamming transition, previously seen only numerically in the full replica-symmetry-breaking solution of hard spheres, is derived from the scaling equations and published after peer review.","field":"physics","date":"2026-06-02","added":"2026-08-11","lab":"Independent","model":"Claude Sonnet 4.6, Claude Opus 4.7","verification":"peer-reviewed","autonomy":"collaborative","tags":["statistical-physics","jamming","critical-exponents"],"humans":["Giorgio Parisi","Francesco Zamponi"],"year_posed":2014,"sources":[{"label":"arXiv: A proof of an identity for the critical exponents of jamming","url":"https://arxiv.org/abs/2606.03300","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"fullrsb-jamming-identity","url":"https://vibemathed.com/problem/fullrsb-jamming-identity","title":"FullRSB Jamming Identity a + b = 1"}],"url":"https://whataifound.org/finding/2026-06-02-jamming-exponent-identity"},{"id":"2026-05-21-alphaproof-nexus","title":"Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs","claim":"An agent pairing language models with the Lean proof assistant resolved 9 of 353 open Erdős problems and 44 of 492 open OEIS conjectures, with every proof mechanically verified.","field":"mathematics","date":"2026-05-21","added":"2026-07-27","lab":"Google DeepMind","model":"AlphaProof Nexus (LLM + Lean)","verification":"formal","autonomy":"search-scaffold","tags":["lean","automated-theorem-proving","erdos-problems","combinatorics"],"humans":["Pushmeet Kohli","Swarat Chaudhuri"],"sources":[{"label":"arXiv: Advancing Mathematics Research with AI-Driven Formal Proof Search","url":"https://arxiv.org/abs/2605.22763","kind":"research"},{"label":"All Lean proofs (DeepMind repository)","url":"https://github.com/google-deepmind/alphaproof-nexus-results","kind":"research"},{"label":"Tao's AI-contributions-to-Erdős-problems wiki","url":"https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems","kind":"research"}],"registrations":[{"registry":"vibemathed","id":"erdos-12","url":"https://vibemathed.com/problem/erdos-12","title":"Erdős Problem #12"},{"registry":"vibemathed","id":"erdos-138","url":"https://vibemathed.com/problem/erdos-138","title":"Erdős Problem #138"},{"registry":"vibemathed","id":"green-open-problem-57","url":"https://vibemathed.com/problem/green-open-problem-57","title":"Ben Green's Open Problem 57"},{"registry":"vibemathed","id":"wow-graph-conjecture-2","url":"https://vibemathed.com/problem/wow-graph-conjecture-2","title":"Written on the Wall II, Graph Conjecture 2"},{"registry":"vibemathed","id":"monochromatic-quantum-graphs-diagonal","url":"https://vibemathed.com/problem/monochromatic-quantum-graphs-diagonal","title":"Monochromatic Quantum Graphs in the Diagonal Family"},{"registry":"vibemathed","id":"monochromatic-quantum-graphs-four-particles","url":"https://vibemathed.com/problem/monochromatic-quantum-graphs-four-particles","title":"Four-Particle Monochromatic Quantum Graphs"},{"registry":"vibemathed","id":"pure-o-sequences-log-concavity","url":"https://vibemathed.com/problem/pure-o-sequences-log-concavity","title":"Log-Concavity of Codimension-Three Pure O-Sequences"},{"registry":"vibemathed","id":"anchored-gda-last-iterate","url":"https://vibemathed.com/problem/anchored-gda-last-iterate","title":"Last-Iterate Rate for Anchored Gradient Descent-Ascent","note":"This record cites the team's April preprint, arXiv:2604.03782, which the AlphaProof Nexus report refers to for this result; the Lean proof sits in the same results repository."}],"url":"https://whataifound.org/finding/2026-05-21-alphaproof-nexus"},{"id":"2026-05-erdos-unit-distance","title":"Disproof of the Erdős unit-distance conjecture","claim":"A reasoning model produced the core construction disproving a 1946 conjecture in discrete geometry, finding point configurations with more unit-distance pairs than the conjecture permitted.","field":"mathematics","date":"2026-05-20","added":"2026-07-20","lab":"OpenAI","model":"GPT-5 series reasoning model","verification":"independent","autonomy":"ai-led","tags":["discrete-geometry","combinatorics","erdos"],"year_posed":1946,"sources":[{"label":"Remarks on the disproof of the unit distance conjecture (human-verified writeup)","url":"https://arxiv.org/abs/2605.20695","kind":"research"},{"label":"Sawin: An explicit lower bound for the unit distance problem","url":"https://arxiv.org/abs/2605.20579","kind":"research"},{"label":"Quanta: The AI Revolution in Math Has Arrived","url":"https://www.quantamagazine.org/the-ai-revolution-in-math-has-arrived-20260413/","kind":"coverage"},{"label":"TechCrunch: OpenAI claims it solved an 80-year-old math problem, for real this time","url":"https://techcrunch.com/2026/05/20/openai-claims-it-solved-an-80-year-old-math-problem-for-real-this-time/","kind":"coverage"},{"label":"Tech Jacks: AI math reasoning milestones","url":"https://techjacksolutions.com/ai-brief/ai-math-reasoning-milestones-30-days-research-automation/","kind":"coverage"}],"registrations":[{"registry":"palomar","id":"PALOMAR-2026-08-08-000001","url":"https://palomar-registry.org/entry?id=PALOMAR-2026-08-08-000001&version=3","repository":"kim-em/erdos-unit-distance-comparator","commit":"be6c2ee4c9fb16fd6bed442b4c361fb10369beb5","theorems":["UnitDistance.erdos_unit_distance_uniform_constant_false"],"checked":"2026-08-14","note":"Palomar's record describes this as certifying the literal negation of the uniform-constant form of the conjecture, from a Mathlib-only statement of that negation. That is narrower than this entry's claim, which is why the entry stays at independently checked rather than moving to formally verified."},{"registry":"mathdb","id":"315785","title":"Erdős unit-distance conjecture","url":"https://mathdb.com/p/315785/erdos-unit-distance-conjecture"}],"url":"https://whataifound.org/finding/2026-05-erdos-unit-distance"},{"id":"2026-05-18-pevac-ps-sarbecovirus","title":"Phase 1 trial of a computationally designed pan-sarbecovirus vaccine","claim":"A vaccine whose antigen was designed entirely in silico from sarbecovirus sequence data was safe in 39 healthy volunteers and raised immune responses against SARS-CoV-2, SARS, and bat viruses that have never infected humans.","field":"medicine","date":"2026-05-18","added":"2026-08-06","lab":"University of Cambridge / DIOSynVax","model":"Unknown","verification":"peer-reviewed","autonomy":"ai-assisted","tags":["vaccine-design","clinical-trial","coronavirus","antigen-design","phase-1"],"humans":["Alasdair P. S. Munro","Jonathan L. Heeney","Saul N. Faust"],"sources":[{"label":"Journal of Infection: A phase I, needle free, dose escalation clinical trial of pEVAC-PS, a candidate pan-Sarbecovirus vaccine","url":"https://www.journalofinfection.com/article/S0163-4453(26)00084-8/fulltext","kind":"research"},{"label":"University of Cambridge: New universal vaccine technology could protect us from future virus outbreaks","url":"https://www.cam.ac.uk/research/news/new-universal-vaccine-technology-could-protect-us-from-future-virus-outbreaks","kind":"announcement"},{"label":"ScienceDaily: AI-designed universal coronavirus vaccine passes first human trial","url":"https://www.sciencedaily.com/releases/2026/06/260605023357.htm","kind":"coverage"}],"url":"https://whataifound.org/finding/2026-05-18-pevac-ps-sarbecovirus"},{"id":"2026-04-23-synthecin","title":"An antibiotic designed by reinforcement learning clears an MRSA infection in mice","claim":"A reinforcement-learning generator searching a 46-billion-compound synthesizable space produced synthecin, a structurally novel antibacterial that cleared a methicillin-resistant Staphylococcus aureus wound infection in a mouse model.","field":"medicine","date":"2026-04-23","added":"2026-08-21","lab":"McMaster University / Stanford University","model":"SyntheMol-RL","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["antibiotics","drug-discovery","reinforcement-learning","generative-model","mrsa","in-vivo"],"humans":["Kyle Swanson","Gary Liu","Denise B. Catacutan","Eric D. Brown","James Zou","Jonathan M. Stokes"],"sources":[{"label":"Molecular Systems Biology: SyntheMol-RL","url":"https://pmc.ncbi.nlm.nih.gov/articles/PMC13230741/","kind":"research"},{"label":"bioRxiv preprint (2025)","url":"https://www.biorxiv.org/content/10.1101/2025.05.17.654017v1","kind":"research"},{"label":"McMaster University announcement","url":"https://news.mcmaster.ca/mcmaster-built-ai-model-speeds-up-drug-discovery-designs-new-antibiotic/","kind":"announcement"}],"url":"https://whataifound.org/finding/2026-04-23-synthecin"},{"id":"2026-01-alphaevolve-bruhat","title":"Structure in Bruhat intervals of permutation groups","claim":"AlphaEvolve identified unexpected special structure in Bruhat intervals for particular permutation groups.","field":"mathematics","date":"2026-01-15","added":"2026-07-20","lab":"Google DeepMind","model":"AlphaEvolve (Gemini-based)","verification":"independent","autonomy":"search-scaffold","tags":["combinatorics","alphaevolve"],"sources":[{"label":"Ellenberg, Libedinsky, Plaza, Simental, Williamson: Bruhat intervals that are large hypercubes","url":"https://arxiv.org/abs/2601.01235","kind":"research"},{"label":"Quanta: The AI Revolution in Math Has Arrived","url":"https://www.quantamagazine.org/the-ai-revolution-in-math-has-arrived-20260413/","kind":"coverage"}],"url":"https://whataifound.org/finding/2026-01-alphaevolve-bruhat"},{"id":"2026-01-erdos-728","title":"Erdős problem #728 resolved and formalized in Lean","claim":"GPT-5.2 produced a proof of a previously open Erdős problem; Harmonic's Aristotle formalized it in Lean, making it the first Erdős problem regarded as fully resolved by AI with machine-checked proof.","field":"mathematics","date":"2026-01-13","added":"2026-07-20","lab":"OpenAI / Harmonic","model":"GPT-5.2 Pro + Aristotle","verification":"formal","autonomy":"autonomous","tags":["number-theory","erdos","lean","formalization"],"sources":[{"label":"arXiv 2601.07421: Resolution of Erdős Problem #728","url":"https://arxiv.org/abs/2601.07421","kind":"research"},{"label":"Tao: AI contributions to Erdős problems","url":"https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems","kind":"research"},{"label":"The Decoder: Tao on GPT-5.2 Pro","url":"https://the-decoder.com/terence-tao-says-gpt-5-2-pro-cracked-an-erdos-problem-but-warns-the-win-says-more-about-speed-than-difficulty/","kind":"coverage"}],"registrations":[{"registry":"mathdb","id":"315787","title":"Erdős Problem #728","url":"https://mathdb.com/p/315787/erdos-problem-728"}],"url":"https://whataifound.org/finding/2026-01-erdos-728"},{"id":"2025-11-gpt5-science-acceleration","title":"Early science acceleration experiments with GPT-5","claim":"A multi-domain study documenting cases where GPT-5 contributed to research progress across mathematics, physics, biology and materials science.","field":"computer-science","date":"2025-11-20","added":"2026-07-20","lab":"OpenAI","model":"GPT-5","verification":"peer-reviewed","autonomy":"ai-assisted","tags":["meta","multi-domain"],"sources":[{"label":"arXiv 2511.16072","url":"https://arxiv.org/pdf/2511.16072","kind":"research"}],"url":"https://whataifound.org/finding/2025-11-gpt5-science-acceleration"},{"id":"2025-11-03-alphaevolve-at-scale","title":"AlphaEvolve across 67 problems: 20 improvements, 8 regressions","claim":"A systematic study with Terence Tao of an evolutionary coding agent on 67 open problems in analysis, combinatorics and geometry, reporting where it beat the literature and where it did not.","field":"mathematics","date":"2025-11-03","added":"2026-07-27","lab":"Google DeepMind","model":"AlphaEvolve (Gemini-based)","verification":"independent","autonomy":"search-scaffold","tags":["combinatorics","geometry","analysis","evolutionary-search"],"humans":["Terence Tao","Javier Gómez-Serrano","Bogdan Georgiev","Adam Zsolt Wagner"],"sources":[{"label":"arXiv: Mathematical exploration and discovery at scale","url":"https://arxiv.org/abs/2511.02864","kind":"research"},{"label":"Terence Tao's write-up","url":"https://terrytao.wordpress.com/2025/11/05/mathematical-exploration-and-discovery-at-scale/","kind":"announcement"}],"url":"https://whataifound.org/finding/2025-11-03-alphaevolve-at-scale"},{"id":"2025-10-19-gpt5-erdos-retrieval","title":"GPT-5 \"solved 10 Erdős problems\": it located existing solutions","claim":"An OpenAI executive announced that GPT-5 had solved 10 previously open Erdős problems and made progress on 11 more; the problems were only 'open' in the sense that one database maintainer was unaware of the already-published solutions the model surfaced.","field":"mathematics","date":"2025-10-19","added":"2026-07-20","lab":"OpenAI","model":"GPT-5","verification":"known","autonomy":"retrieval","tags":["number-theory","erdos","already-known","cautionary","retrieval"],"sources":[{"label":"TechCrunch: OpenAI's 'embarrassing' math","url":"https://techcrunch.com/2025/10/19/openais-embarrassing-math/","kind":"challenge"},{"label":"The Decoder: A GPT-5 math breakthrough that never happened","url":"https://the-decoder.com/leading-openai-researcher-announced-a-gpt-5-math-breakthrough-that-never-happened/","kind":"challenge"}],"url":"https://whataifound.org/finding/2025-10-19-gpt5-erdos-retrieval"},{"id":"2025-09-25-qma-amplification-limits","title":"Limits to black-box amplification in QMA, with the key step written by GPT-5","claim":"A quantum complexity paper proving black-box error amplification for QMA cannot push completeness closer to certainty than doubly exponentially, in which the pivotal technical step was produced by GPT-5 in about half an hour.","field":"computer-science","date":"2025-09-25","added":"2026-07-29","lab":"UT Austin / CWI Amsterdam","model":"GPT-5 Thinking","verification":"author-verified","autonomy":"ai-assisted","tags":["quantum-complexity","proof-assistance","oracle-separation"],"humans":["Scott Aaronson","Freek Witteveen"],"sources":[{"label":"arXiv: Limits to black-box amplification in QMA","url":"https://arxiv.org/abs/2509.21131","kind":"research"},{"label":"Scott Aaronson: The QMA Singularity","url":"https://scottaaronson.blog/?p=9183","kind":"announcement"}],"url":"https://whataifound.org/finding/2025-09-25-qma-amplification-limits"},{"id":"2025-09-17-evo-phage-genomes","title":"AI-generated bacteriophage genomes that replicate and kill bacteria","claim":"Genome language models wrote complete ΦX174-like bacteriophage genomes from scratch; of 285 designs that could be built, 16 produced viable infectious phages, several with faster lysis than the natural virus.","field":"biology","date":"2025-09-17","added":"2026-07-29","lab":"Arc Institute / Stanford University","model":"Evo 1 and Evo 2","verification":"peer-reviewed","autonomy":"ai-led","tags":["genome-design","bacteriophage","generative-biology","biosecurity"],"humans":["Samuel King","Brian Hie"],"sources":[{"label":"Science: Generative design of bacteriophages with genome language models","url":"https://www.science.org/doi/10.1126/science.aec2657","kind":"research"},{"label":"bioRxiv: Generative design of novel bacteriophages with genome language models","url":"https://www.biorxiv.org/content/10.1101/2025.09.12.675911v1","kind":"research"},{"label":"Arc Institute: How we built the first AI-generated genomes","url":"https://arcinstitute.org/news/hie-king-first-synthetic-phage","kind":"announcement"},{"label":"Asimov Press: AI-designed phages","url":"https://www.asimov.press/p/ai-phages","kind":"coverage"},{"label":"Inglesby and Hanke: Guarding against the misuse of AI-designed viruses","url":"https://www.science.org/doi/10.1126/science.aej8512","kind":"commentary"}],"url":"https://whataifound.org/finding/2025-09-17-evo-phage-genomes"},{"id":"2025-09-17-unstable-singularities","title":"New families of unstable singularities in fluid equations","claim":"Physics-informed neural networks found previously unknown unstable self-similar blow-up solutions for three fluid equations, computed to near machine precision, and revealed an unexpected near-linear relation between a solution's instability order and its blow-up rate.","field":"mathematics","date":"2025-09-17","added":"2026-07-29","lab":"Google DeepMind (with Brown, NYU and Stanford)","model":"Physics-informed neural networks with Gauss–Newton optimisation","verification":"author-verified","autonomy":"search-scaffold","tags":["pde","fluid-dynamics","singularity","physics-informed-neural-networks"],"humans":["Javier Gómez-Serrano","Tristan Buckmaster","Ching-Yao Lai","Yongji Wang"],"sources":[{"label":"arXiv: Discovery of Unstable Singularities","url":"https://arxiv.org/abs/2509.14185","kind":"research"},{"label":"DeepMind: Discovering new solutions to century-old problems in fluid dynamics","url":"https://deepmind.google/blog/discovering-new-solutions-to-century-old-problems-in-fluid-dynamics/","kind":"announcement"},{"label":"Physics World: Neural networks discover unstable singularities in fluid systems","url":"https://physicsworld.com/a/neural-networks-discover-unstable-singularities-in-fluid-systems/","kind":"coverage"}],"url":"https://whataifound.org/finding/2025-09-17-unstable-singularities"},{"id":"2025-09-11-gauss-strong-pnt","title":"Strong prime number theorem formalized in Lean by an autoformalization agent","claim":"An agent completed a Lean formalization of the strong prime number theorem in about three weeks, finishing a project two expert mathematicians had left blocked after 18 months.","field":"mathematics","date":"2025-09-11","added":"2026-07-27","lab":"Math, Inc.","model":"Gauss (autoformalization agent)","verification":"author-verified","autonomy":"ai-assisted","tags":["lean","formalization","number-theory","prime-number-theorem"],"humans":["Terence Tao","Alex Kontorovich"],"sources":[{"label":"Math, Inc.: Introducing Gauss","url":"https://www.math.inc/gauss","kind":"announcement"},{"label":"strongpnt Lean repository","url":"https://github.com/math-inc/strongpnt","kind":"research"}],"url":"https://whataifound.org/finding/2025-09-11-gauss-strong-pnt"},{"id":"2025-08-gpt5-convex-bound","title":"Improved step-size bound in smooth convex optimization","claim":"GPT-5 Pro extended a guaranteed-convexity window for gradient descent from \\(\\eta \\le 1/L\\) to \\(\\eta \\le 1.5/L\\), but the optimal \\(1.75/L\\) bound had already been published months earlier.","field":"mathematics","date":"2025-08-01","added":"2026-07-20","lab":"OpenAI","model":"GPT-5 Pro","verification":"known","autonomy":"ai-assisted","tags":["optimization","already-known","cautionary"],"humans":["Sébastien Bubeck"],"sources":[{"label":"Analysis of the claim","url":"https://hackmd.io/@niloydebbarma/HkGxVPwFgx","kind":"challenge"},{"label":"What does GPT-5's 'new math' claim actually mean?","url":"https://allthings.how/what-does-gpt-5s-new-math-claim-actually-mean/","kind":"challenge"}],"url":"https://whataifound.org/finding/2025-08-gpt5-convex-bound"},{"id":"2025-07-28-aristotle-imo-lean","title":"Machine-checked Lean proofs for five of six 2025 IMO problems","claim":"Harmonic's Aristotle produced formally verified Lean 4 proofs for five of the six 2025 IMO problems, so the gold-medal-standard score rests on a compiler rather than on human graders.","field":"mathematics","date":"2025-07-28","added":"2026-07-29","lab":"Harmonic","model":"Aristotle","verification":"formal","autonomy":"ai-led","tags":["olympiad","lean","formalization","benchmark"],"sources":[{"label":"arXiv: Aristotle: IMO-level Automated Theorem Proving","url":"https://arxiv.org/abs/2510.01346","kind":"research"},{"label":"harmonic-ai/IMO2025: Lean proofs and verification artifacts","url":"https://github.com/harmonic-ai/IMO2025","kind":"research"}],"url":"https://whataifound.org/finding/2025-07-28-aristotle-imo-lean"},{"id":"2025-07-21-gemini-deepthink-imo","title":"Gold-medal standard at the 2025 International Mathematical Olympiad","claim":"An advanced version of Gemini Deep Think read the official problem statements and wrote natural-language proofs for five of the six 2025 IMO problems inside the contest time limits, scoring 35 of 42, graded and certified by the official IMO coordinators.","field":"mathematics","date":"2025-07-21","added":"2026-07-29","lab":"Google DeepMind","model":"Gemini Deep Think (advanced version)","verification":"independent","autonomy":"ai-led","tags":["olympiad","benchmark","natural-language-proof"],"sources":[{"label":"Gemini Deep Think: official IMO 2025 solutions (PDF)","url":"https://storage.googleapis.com/deepmind-media/gemini/IMO_2025.pdf","kind":"research"},{"label":"DeepMind: Gemini with Deep Think officially achieves gold-medal standard at the IMO","url":"https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/","kind":"announcement"},{"label":"Simon Willison: OpenAI's gold medal performance on the IMO","url":"https://simonwillison.net/2025/Jul/19/openai-gold-medal-math-olympiad/","kind":"commentary"}],"url":"https://whataifound.org/finding/2025-07-21-gemini-deepthink-imo"},{"id":"2025-06-03-rentosertib-phase2a","title":"Phase 2a results for a drug whose target and molecule both came from AI","claim":"Rentosertib, a TNIK inhibitor whose target was picked by one AI system and whose molecule was generated by another, improved forced vital capacity by 98.4 mL at the top dose against a 20.3 mL decline on placebo in a 71-patient randomised trial.","field":"medicine","date":"2025-06-03","added":"2026-07-29","lab":"Insilico Medicine","model":"PandaOmics (target) + Chemistry42 (molecule)","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["drug-discovery","clinical-trial","target-discovery","fibrosis"],"sources":[{"label":"Nature Medicine: A generative AI-discovered TNIK inhibitor for idiopathic pulmonary fibrosis","url":"https://www.nature.com/articles/s41591-025-03743-2","kind":"research"},{"label":"Insilico Medicine: positive topline results of ISM001-055","url":"https://insilico.com/news/tnik-ipf-phase2a","kind":"announcement"}],"url":"https://whataifound.org/finding/2025-06-03-rentosertib-phase2a"},{"id":"2025-05-alphaevolve-kissing","title":"Improved lower bound for the 11-dimensional kissing number","claim":"AlphaEvolve improved the best known configuration for the kissing number problem in 11 dimensions.","field":"mathematics","date":"2025-05-14","added":"2026-07-20","lab":"Google DeepMind","model":"AlphaEvolve (Gemini-based)","verification":"independent","autonomy":"search-scaffold","tags":["geometry","sphere-packing","alphaevolve"],"year_posed":1694,"sources":[{"label":"AlphaEvolve paper (PDF)","url":"https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/AlphaEvolve.pdf","kind":"research"},{"label":"DeepMind: AlphaEvolve","url":"https://deepmind.google/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/","kind":"announcement"},{"label":"IEEE Spectrum: AlphaEvolve Tackles Kissing Problem","url":"https://spectrum.ieee.org/deepmind-alphaevolve","kind":"coverage"}],"registrations":[{"registry":"mathdb","id":"315951","title":"Kissing number problem","url":"https://mathdb.com/p/315951/kissing-number-problem"}],"url":"https://whataifound.org/finding/2025-05-alphaevolve-kissing"},{"id":"2025-05-alphaevolve-matmul","title":"4×4 complex matrix multiplication in 48 scalar multiplications","claim":"AlphaEvolve found a scheme multiplying 4×4 complex matrices with 48 scalar multiplications, improving on Strassen's 49 from 1969.","field":"computer-science","date":"2025-05-14","added":"2026-07-20","lab":"Google DeepMind","model":"AlphaEvolve (Gemini-based)","verification":"independent","autonomy":"search-scaffold","tags":["algorithms","linear-algebra","alphaevolve"],"year_posed":1969,"sources":[{"label":"AlphaEvolve paper (PDF)","url":"https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/AlphaEvolve.pdf","kind":"research"},{"label":"DeepMind: AlphaEvolve","url":"https://deepmind.google/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/","kind":"announcement"},{"label":"IEEE Spectrum","url":"https://spectrum.ieee.org/deepmind-alphaevolve","kind":"coverage"},{"label":"Wikipedia: AlphaEvolve","url":"https://en.wikipedia.org/wiki/AlphaEvolve","kind":"commentary"}],"url":"https://whataifound.org/finding/2025-05-alphaevolve-matmul"},{"id":"2025-05-alphaevolve-minimum-overlap","title":"Improved bound for the Erdős minimum-overlap problem","claim":"AlphaEvolve nudged the best known bound for Erdős's minimum-overlap constant, the first improvement since 2016, and sharpened several autocorrelation inequalities.","field":"mathematics","date":"2025-05-14","added":"2026-07-21","lab":"Google DeepMind","model":"AlphaEvolve (Gemini-based)","verification":"independent","autonomy":"search-scaffold","tags":["analysis","erdos","alphaevolve"],"year_posed":1955,"sources":[{"label":"DeepMind: AlphaEvolve","url":"https://deepmind.google/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/","kind":"announcement"},{"label":"AlphaEvolve paper (PDF)","url":"https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/AlphaEvolve.pdf","kind":"research"},{"label":"Wikipedia: Minimum overlap problem","url":"https://en.wikipedia.org/wiki/Minimum_overlap_problem","kind":"commentary"}],"registrations":[{"registry":"mathdb","id":"316064","title":"Minimum overlap problem","url":"https://mathdb.com/p/316064/minimum-overlap-problem"}],"url":"https://whataifound.org/finding/2025-05-alphaevolve-minimum-overlap"},{"id":"2025-robin-macular","title":"Candidate treatment for dry age-related macular degeneration","claim":"The Robin system automated hypothesis generation, experiment design and data analysis, identifying a novel candidate treatment for dry AMD.","field":"biology","date":"2025-05-01","added":"2026-07-20","lab":"FutureHouse","model":"Robin (multi-agent)","verification":"peer-reviewed","autonomy":"ai-led","tags":["drug-discovery","ophthalmology","multi-agent"],"sources":[{"label":"Nature: A multi-agent system for automating scientific discovery","url":"https://www.nature.com/articles/s41586-026-10652-y","kind":"research"},{"label":"Turing Post: 12 AI Co-Scientists of 2026","url":"https://www.turingpost.com/p/ai-co-scientists-in-2026","kind":"coverage"}],"url":"https://whataifound.org/finding/2025-robin-macular"},{"id":"2025-03-12-ai-scientist-workshop-paper","title":"A fully machine-generated paper passed workshop peer review","claim":"One of three end-to-end AI-generated manuscripts submitted to an ICLR 2025 workshop averaged 6.33 from reviewers and would have been accepted; the authors withdrew it, and the bar cleared was a workshop track, not the main conference.","field":"computer-science","date":"2025-03-12","added":"2026-07-29","lab":"Sakana AI","model":"The AI Scientist-v2","verification":"author-verified","autonomy":"ai-led","tags":["autonomous-research","peer-review","agents","contested"],"sources":[{"label":"Sakana AI: The AI Scientist generates its first peer-reviewed publication","url":"https://sakana.ai/ai-scientist-first-publication/","kind":"announcement"},{"label":"TechCrunch: Sakana claims its AI paper passed peer review (it's more nuanced than that)","url":"https://techcrunch.com/2025/03/12/sakana-claims-its-ai-paper-passed-peer-review-but-its-a-bit-more-nuanced-than-that/","kind":"challenge"},{"label":"SakanaAI/AI-Scientist-ICLR2025-Workshop-Experiment (manuscripts and reviews)","url":"https://github.com/SakanaAI/AI-Scientist-ICLR2025-Workshop-Experiment","kind":"research"}],"url":"https://whataifound.org/finding/2025-03-12-ai-scientist-workshop-paper"},{"id":"2025-02-ai-coscientist-amr","title":"AI co-scientist hypotheses on antimicrobial resistance and liver fibrosis","claim":"A multi-agent system generated hypotheses that were subsequently validated experimentally in the lab.","field":"biology","date":"2025-02-19","added":"2026-07-20","lab":"Google","model":"AI Co-Scientist (Gemini 2.0 multi-agent)","verification":"peer-reviewed","autonomy":"ai-assisted","tags":["hypothesis-generation","microbiology","multi-agent"],"sources":[{"label":"Nature: Accelerating scientific discovery with Co-Scientist","url":"https://www.nature.com/articles/s41586-026-10644-y","kind":"research"},{"label":"bioRxiv: AI mirrors experimental science to uncover a novel mechanism of gene transfer","url":"https://www.biorxiv.org/content/10.1101/2025.02.19.639094v1","kind":"research"},{"label":"Turing Post: 12 AI Co-Scientists of 2026","url":"https://www.turingpost.com/p/ai-co-scientists-in-2026","kind":"coverage"}],"url":"https://whataifound.org/finding/2025-02-ai-coscientist-amr"},{"id":"2025-02-13-designed-serine-hydrolases","title":"Enzymes with working catalytic machinery designed from scratch","claim":"Diffusion-based protein design produced serine hydrolases with catalytic efficiencies up to \\(2.2 \\times 10^5\\ \\mathrm{M^{-1}\\,s^{-1}}\\) on five folds unlike any natural serine hydrolase, with crystal structures matching the design models to under 1 Å.","field":"chemistry","date":"2025-02-13","added":"2026-07-29","lab":"Institute for Protein Design, University of Washington","model":"RFdiffusion with PLACER ensemble scoring","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["protein-design","enzyme-design","rfdiffusion","catalysis"],"humans":["Anna Lauko","David Baker"],"sources":[{"label":"Science: Computational design of serine hydrolases","url":"https://www.science.org/doi/10.1126/science.adu2454","kind":"research"},{"label":"Baker Lab: Generating new enzymes with complex active sites","url":"https://www.bakerlab.org/2025/02/13/ai-enzymes-with-complex-active-sites/","kind":"announcement"}],"url":"https://whataifound.org/finding/2025-02-13-designed-serine-hydrolases"},{"id":"2025-01-16-esmgfp","title":"A working fluorescent protein generated by a language model","claim":"ESM3 designed esmGFP, a bright green fluorescent protein sharing only 58% of its sequence with the closest known natural fluorescent protein, a distance the authors estimate at over 500 million years of natural evolution.","field":"biology","date":"2025-01-16","added":"2026-07-29","lab":"EvolutionaryScale","model":"ESM3 (98B)","verification":"peer-reviewed","autonomy":"ai-led","tags":["protein-design","generative-biology","fluorescent-protein"],"humans":["Alexander Rives","Tom Sercu"],"sources":[{"label":"Science: Simulating 500 million years of evolution with a language model","url":"https://www.science.org/doi/10.1126/science.ads0018","kind":"research"},{"label":"EvolutionaryScale: ESM3 release","url":"https://www.evolutionaryscale.ai/blog/esm3-release","kind":"announcement"}],"url":"https://whataifound.org/finding/2025-01-16-esmgfp"},{"id":"2025-01-16-mattergen","title":"Generative model designs crystals to order; its flagship synthesis turned out to be a known compound","claim":"MatterGen generates crystal structures conditioned on target properties, and its headline experimental validation was later shown to match a compound reported in 1972 that sits in the model's own training data.","field":"materials","date":"2025-01-16","added":"2026-07-29","lab":"Microsoft Research","model":"MatterGen","verification":"disputed","autonomy":"search-scaffold","tags":["materials","crystal-structure","diffusion-model","contested"],"sources":[{"label":"Nature: A generative model for inorganic materials design","url":"https://www.nature.com/articles/s41586-025-08628-5","kind":"research"},{"label":"MatterGen code and model weights","url":"https://github.com/microsoft/mattergen","kind":"research"},{"label":"Microsoft Research: MatterGen, a new paradigm of materials design with generative AI","url":"https://www.microsoft.com/en-us/research/blog/mattergen-a-new-paradigm-of-materials-design-with-generative-ai/","kind":"announcement"},{"label":"Materials Horizons: MatterGen predicts compounds from the training dataset","url":"https://pubs.rsc.org/en/content/articlelanding/2026/mh/d6mh00268d","kind":"challenge"}],"url":"https://whataifound.org/finding/2025-01-16-mattergen"},{"id":"2024-11-20-alphaqubit","title":"A neural decoder that identifies quantum errors more accurately than hand-designed methods","claim":"A transformer trained on Google's Sycamore surface-code data cut decoding errors by 6% against tensor-network decoding and 30% against correlated matching, the best reported accuracy at the time.","field":"physics","date":"2024-11-20","added":"2026-07-29","lab":"Google DeepMind / Google Quantum AI","model":"AlphaQubit","verification":"peer-reviewed","autonomy":"ai-led","tags":["quantum-computing","error-correction","transformer"],"sources":[{"label":"Nature: Learning high-accuracy error decoding for quantum processors","url":"https://www.nature.com/articles/s41586-024-08148-8","kind":"research"},{"label":"Google: AlphaQubit, research on quantum error correction","url":"https://blog.google/innovation-and-ai/models-and-research/google-deepmind/alphaqubit-quantum-error-correction/","kind":"announcement"}],"url":"https://whataifound.org/finding/2024-11-20-alphaqubit"},{"id":"2024-10-02-flywire-connectome","title":"Complete wiring diagram of an adult fruit-fly brain","claim":"Machine segmentation of an electron-microscopy volume, corrected by a large community of proofreaders, produced the first synapse-level map of an entire adult brain: 139,255 neurons and roughly 50 million synapses.","field":"neuroscience","date":"2024-10-02","added":"2026-07-29","lab":"FlyWire Consortium (Princeton, MRC LMB, Cambridge, Vermont)","model":"Automated electron-microscopy segmentation networks","verification":"peer-reviewed","autonomy":"ai-assisted","tags":["connectome","electron-microscopy","segmentation","drosophila"],"humans":["Sebastian Seung","Mala Murthy","Gregory Jefferis"],"sources":[{"label":"Nature: Neuronal wiring diagram of an adult brain","url":"https://www.nature.com/articles/s41586-024-07558-y","kind":"research"},{"label":"NIH: Complete wiring map of an adult fruit fly brain","url":"https://www.nih.gov/news-events/nih-research-matters/complete-wiring-map-adult-fruit-fly-brain","kind":"announcement"},{"label":"FlyWire (data and explorer)","url":"https://flywire.ai/","kind":"research"}],"url":"https://whataifound.org/finding/2024-10-02-flywire-connectome"},{"id":"2024-07-25-alphaproof-imo","title":"Silver-medal standard at the 2024 International Mathematical Olympiad","claim":"AlphaProof and AlphaGeometry 2 together solved four of the six 2024 IMO problems for 28 of 42 points (one short of the gold threshold), with the algebra and number-theory solutions produced and checked in the Lean proof assistant.","field":"mathematics","date":"2024-07-25","added":"2026-07-20","lab":"Google DeepMind","model":"AlphaProof + AlphaGeometry 2","verification":"independent","autonomy":"ai-led","tags":["olympiad","lean","formalization","benchmark"],"sources":[{"label":"DeepMind: AI achieves silver-medal standard solving IMO problems","url":"https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/","kind":"announcement"},{"label":"Nature: Olympiad-level formal mathematical reasoning with reinforcement learning","url":"https://www.nature.com/articles/s41586-025-09833-y","kind":"research"},{"label":"Unite.AI: How AlphaProof and AlphaGeometry 2 achieved silver-medal standard","url":"https://www.unite.ai/ai-at-the-international-mathematical-olympiad-how-alphaproof-and-alphageometry-2-achieved-silver-medal-standard/","kind":"coverage"}],"url":"https://whataifound.org/finding/2024-07-25-alphaproof-imo"},{"id":"2024-05-08-alphafold3","title":"Joint structure prediction for proteins, nucleic acids and ligands (AlphaFold 3)","claim":"A diffusion-based successor to AlphaFold predicts complexes spanning proteins, DNA, RNA, small molecules and ions in a single model, with large accuracy gains over the specialised docking tools used for each case.","field":"biology","date":"2024-05-08","added":"2026-07-29","lab":"Google DeepMind / Isomorphic Labs","model":"AlphaFold 3","verification":"peer-reviewed","autonomy":"ai-led","tags":["protein-structure","drug-discovery","alphafold","diffusion-model"],"humans":["John Jumper","Max Jaderberg"],"sources":[{"label":"Nature: Accurate structure prediction of biomolecular interactions with AlphaFold 3","url":"https://www.nature.com/articles/s41586-024-07487-w","kind":"research"},{"label":"AlphaFold 3 code (google-deepmind/alphafold3)","url":"https://github.com/google-deepmind/alphafold3","kind":"research"},{"label":"Google DeepMind and Isomorphic Labs introduce AlphaFold 3","url":"https://blog.google/innovation-and-ai/products/google-deepmind-isomorphic-alphafold-3-ai-model/","kind":"announcement"},{"label":"bioRxiv: Have protein-ligand co-folding methods moved beyond memorisation?","url":"https://www.biorxiv.org/content/10.1101/2025.02.03.636309v3","kind":"challenge"}],"url":"https://whataifound.org/finding/2024-05-08-alphafold3"},{"id":"2024-02-21-tearing-mode-avoidance","title":"Reinforcement learning steers a tokamak away from tearing instabilities","claim":"A controller trained on past DIII-D shots forecast tearing-mode instabilities up to 300 ms ahead and adjusted the plasma in real time to avoid them, holding high-performance conditions that would otherwise have collapsed.","field":"physics","date":"2024-02-21","added":"2026-07-29","lab":"Princeton University / PPPL / DIII-D National Fusion Facility","model":"Deep reinforcement learning controller over a learned plasma model","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["fusion","plasma-control","reinforcement-learning","tokamak"],"humans":["Jaemin Seo","Egemen Kolemen"],"sources":[{"label":"Nature: Avoiding fusion plasma tearing instability with deep reinforcement learning","url":"https://www.nature.com/articles/s41586-024-07024-9","kind":"research"},{"label":"Princeton Engineering: Engineers use AI to wrangle fusion power for the grid","url":"https://engineering.princeton.edu/news/2024/02/21/engineers-use-ai-wrangle-fusion-power-grid","kind":"announcement"}],"url":"https://whataifound.org/finding/2024-02-21-tearing-mode-avoidance"},{"id":"2024-01-17-alphageometry","title":"Olympiad geometry solved without human demonstrations","claim":"A language model trained purely on synthetic data, paired with a symbolic deduction engine, solved 25 of 30 olympiad geometry problems against 10 for the previous best automated system and 25.9 for the average human gold medallist.","field":"mathematics","date":"2024-01-17","added":"2026-07-29","lab":"Google DeepMind","model":"AlphaGeometry","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["olympiad","geometry","neuro-symbolic","benchmark"],"humans":["Trieu Trinh","Thang Luong"],"sources":[{"label":"Nature: Solving olympiad geometry without human demonstrations","url":"https://www.nature.com/articles/s41586-023-06747-5","kind":"research"},{"label":"DeepMind: AlphaGeometry, an olympiad-level AI system for geometry","url":"https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/","kind":"announcement"},{"label":"google-deepmind/alphageometry (code)","url":"https://github.com/google-deepmind/alphageometry","kind":"research"},{"label":"arXiv: Wu's method can boost symbolic AI to rival silver medalists and AlphaGeometry to outperform gold medalists","url":"https://arxiv.org/abs/2404.06405","kind":"challenge"}],"url":"https://whataifound.org/finding/2024-01-17-alphageometry"},{"id":"2023-12-20-antibiotic-structural-class","title":"A new structural class of antibiotic candidates against MRSA","claim":"Graph neural networks trained on 39,312 assayed compounds and applied to 12 million molecules surfaced a chemical class active against MRSA in mice, with the substructures driving each prediction made explicit rather than left opaque.","field":"chemistry","date":"2023-12-20","added":"2026-07-29","lab":"MIT / Broad Institute / Harvard","model":"Ensembles of graph neural networks with substructure attribution","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["antibiotics","graph-neural-network","explainability","mrsa"],"humans":["Felix Wong","Erica Zheng","James Collins"],"sources":[{"label":"Nature: Discovery of a structural class of antibiotics with explainable deep learning","url":"https://www.nature.com/articles/s41586-023-06887-8","kind":"research"},{"label":"ScienceDaily: Using AI, researchers identify a new class of antibiotic candidates","url":"https://www.sciencedaily.com/releases/2023/12/231221012744.htm","kind":"coverage"}],"url":"https://whataifound.org/finding/2023-12-20-antibiotic-structural-class"},{"id":"2023-12-20-coscientist","title":"A language-model agent that planned and ran chemistry experiments on lab robots","claim":"Coscientist, driven by GPT-4 with web search, documentation search, code execution and lab automation, designed and executed palladium-catalysed cross-coupling reactions on real robotic hardware from a one-line goal.","field":"chemistry","date":"2023-12-20","added":"2026-07-29","lab":"Carnegie Mellon University","model":"GPT-4 (Coscientist agent)","verification":"peer-reviewed","autonomy":"ai-led","tags":["lab-automation","agents","cross-coupling","self-driving-lab"],"humans":["Daniil Boiko","Robert MacKnight","Gabe Gomes"],"sources":[{"label":"Nature: Autonomous chemical research with large language models","url":"https://www.nature.com/articles/s41586-023-06792-0","kind":"research"},{"label":"PubMed Central full text","url":"https://pmc.ncbi.nlm.nih.gov/articles/PMC10733136/","kind":"research"},{"label":"Coscientist data and reference implementation","url":"https://github.com/gomesgroup/coscientist","kind":"research"}],"url":"https://whataifound.org/finding/2023-12-20-coscientist"},{"id":"2023-12-funsearch-binpacking","title":"Improved heuristics for online bin packing","claim":"FunSearch produced bin-packing heuristics outperforming standard baselines on benchmark distributions.","field":"computer-science","date":"2023-12-14","added":"2026-07-20","lab":"Google DeepMind","model":"FunSearch (PaLM 2 / Codey)","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["algorithms","heuristics","funsearch"],"year_posed":1971,"sources":[{"label":"Nature: Mathematical discoveries from program search with LLMs","url":"https://www.nature.com/articles/s41586-023-06924-6","kind":"research"},{"label":"FunSearch code and discovered programs","url":"https://github.com/google-deepmind/funsearch","kind":"research"}],"url":"https://whataifound.org/finding/2023-12-funsearch-binpacking"},{"id":"2023-12-funsearch-capset","title":"New lower bound constructions for the cap set problem","claim":"FunSearch discovered larger cap sets than any previously known construction, the first time an LLM-based system produced a genuinely new discovery on an established open problem.","field":"mathematics","date":"2023-12-14","added":"2026-07-20","lab":"Google DeepMind","model":"FunSearch (PaLM 2 / Codey)","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["combinatorics","cap-set","funsearch","historic-first"],"year_posed":1970,"sources":[{"label":"Nature: Mathematical discoveries from program search with LLMs","url":"https://www.nature.com/articles/s41586-023-06924-6","kind":"research"},{"label":"FunSearch code and discovered programs","url":"https://github.com/google-deepmind/funsearch","kind":"research"},{"label":"DeepMind: FunSearch","url":"https://deepmind.google/blog/funsearch-making-new-discoveries-in-mathematical-sciences-using-large-language-models/","kind":"announcement"}],"url":"https://whataifound.org/finding/2023-12-funsearch-capset"},{"id":"2023-11-29-a-lab-synthesis","title":"Autonomous laboratory reports solid-state synthesis of new inorganic compounds","claim":"Berkeley's A-Lab, an AI-driven autonomous laboratory, reported synthesising 41 novel inorganic compounds out of 58 targets over 17 days with minimal human intervention.","field":"materials","date":"2023-11-29","added":"2026-07-20","lab":"Lawrence Berkeley National Laboratory","model":"A-Lab (ML planning + robotics)","verification":"disputed","autonomy":"ai-led","tags":["materials","autonomous-lab","synthesis","contested"],"sources":[{"label":"Nature: An autonomous laboratory for the accelerated synthesis of inorganic materials","url":"https://www.nature.com/articles/s41586-023-06734-w","kind":"research"},{"label":"The Register: Boffins deem DeepMind's material discoveries shallow","url":"https://www.theregister.com/2024/04/11/google_deepmind_material_study/","kind":"challenge"}],"url":"https://whataifound.org/finding/2023-11-29-a-lab-synthesis"},{"id":"2023-11-29-gnome","title":"Large-scale prediction of new stable crystalline materials (GNoME)","claim":"GNoME predicted about 2.2 million new inorganic crystal structures, roughly 380,000 of them flagged as thermodynamically stable, presented as an order-of-magnitude expansion of known stable materials.","field":"materials","date":"2023-11-29","added":"2026-07-20","lab":"Google DeepMind","model":"GNoME (graph neural network)","verification":"disputed","autonomy":"search-scaffold","tags":["materials","crystal-structure","graph-neural-network","contested"],"sources":[{"label":"Nature: Scaling deep learning for materials discovery","url":"https://www.nature.com/articles/s41586-023-06735-9","kind":"research"},{"label":"GNoME models, DFT data and 380k predicted structures","url":"https://github.com/google-deepmind/materials_discovery","kind":"research"},{"label":"DeepMind: Millions of new materials discovered with deep learning","url":"https://deepmind.google/blog/millions-of-new-materials-discovered-with-deep-learning/","kind":"announcement"},{"label":"The Register: Boffins deem DeepMind's material discoveries shallow","url":"https://www.theregister.com/2024/04/11/google_deepmind_material_study/","kind":"challenge"}],"url":"https://whataifound.org/finding/2023-11-29-gnome"},{"id":"2023-11-14-graphcast","title":"Medium-range weather forecasts from a graph neural network beat the operational physics model","claim":"GraphCast produced more accurate 10-day forecasts than ECMWF's HRES on roughly 90% of the evaluated variable and lead-time combinations, in under a minute on a single TPU against hours on a supercomputer.","field":"climate","date":"2023-11-14","added":"2026-07-29","lab":"Google DeepMind","model":"GraphCast","verification":"peer-reviewed","autonomy":"ai-led","tags":["weather","forecasting","graph-neural-network"],"humans":["Remi Lam","Peter Battaglia"],"sources":[{"label":"Science: Learning skillful medium-range global weather forecasting","url":"https://www.science.org/doi/10.1126/science.adi2336","kind":"research"},{"label":"DeepMind: GraphCast, AI model for faster and more accurate global weather forecasting","url":"https://deepmind.google/blog/graphcast-ai-model-for-faster-and-more-accurate-global-weather-forecasting/","kind":"announcement"},{"label":"GraphCast code and weights (google-deepmind/weathernext)","url":"https://github.com/google-deepmind/weathernext","kind":"research"}],"url":"https://whataifound.org/finding/2023-11-14-graphcast"},{"id":"2023-09-19-alphamissense","title":"Pathogenicity predictions for 71 million human missense variants","claim":"An AlphaFold-derived model classified 89% of all 71 million possible human missense variants as likely benign or likely pathogenic, against the roughly 0.1% that carry a clinical classification today.","field":"medicine","date":"2023-09-19","added":"2026-07-29","lab":"Google DeepMind","model":"AlphaMissense","verification":"peer-reviewed","autonomy":"ai-led","tags":["genomics","variant-effect","clinical-genetics"],"sources":[{"label":"Science: Accurate proteome-wide missense variant effect prediction with AlphaMissense","url":"https://www.science.org/doi/10.1126/science.adg7492","kind":"research"},{"label":"DeepMind: A catalogue of genetic mutations to help pinpoint the cause of diseases","url":"https://deepmind.google/blog/a-catalogue-of-genetic-mutations-to-help-pinpoint-the-cause-of-diseases/","kind":"announcement"},{"label":"Nature Biotechnology: Advancing missense variant pathogenicity prediction","url":"https://www.nature.com/articles/s41587-023-01999-y","kind":"research"},{"label":"AlphaMissense predictions and code","url":"https://github.com/google-deepmind/alphamissense","kind":"research"}],"url":"https://whataifound.org/finding/2023-09-19-alphamissense"},{"id":"2023-06-07-alphadev","title":"Faster sorting routines discovered and merged into the LLVM C++ library","claim":"AlphaDev found shorter branchless routines for sorting small fixed-length inputs; reverse-engineered to C++, they were merged into LLVM's libc++, the first change to those routines in over a decade.","field":"computer-science","date":"2023-06-07","added":"2026-07-20","lab":"Google DeepMind","model":"AlphaDev (AlphaZero-based)","verification":"independent","autonomy":"search-scaffold","tags":["algorithms","sorting","reinforcement-learning","deployed"],"sources":[{"label":"Nature: Faster sorting algorithms discovered using deep reinforcement learning","url":"https://www.nature.com/articles/s41586-023-06004-9","kind":"research"},{"label":"AlphaDev code and discovered sorting routines","url":"https://github.com/google-deepmind/alphadev","kind":"research"},{"label":"DeepMind: AlphaDev discovers faster sorting algorithms","url":"https://deepmind.google/blog/alphadev-discovers-faster-sorting-algorithms/","kind":"announcement"},{"label":"Wikipedia: AlphaDev","url":"https://en.wikipedia.org/wiki/AlphaDev","kind":"commentary"}],"url":"https://whataifound.org/finding/2023-06-07-alphadev"},{"id":"2022-10-05-alphatensor","title":"Faster matrix-multiplication algorithms found by reinforcement learning","claim":"AlphaTensor discovered matrix-multiplication schemes using fewer scalar multiplications than any previously known, including a way to multiply 4×4 matrices over GF(2) in 47 multiplications versus the 49 of two-level Strassen.","field":"computer-science","date":"2022-10-05","added":"2026-07-20","lab":"Google DeepMind","model":"AlphaTensor (AlphaZero-based)","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["algorithms","linear-algebra","reinforcement-learning"],"year_posed":1969,"sources":[{"label":"Nature: Discovering faster matrix multiplication algorithms with reinforcement learning","url":"https://www.nature.com/articles/s41586-022-05172-4","kind":"research"},{"label":"AlphaTensor code and discovered algorithms","url":"https://github.com/google-deepmind/alphatensor","kind":"research"},{"label":"DeepMind: Discovering novel algorithms with AlphaTensor","url":"https://deepmind.google/discover/blog/discovering-novel-algorithms-with-alphatensor/","kind":"announcement"},{"label":"Quanta: AI Reveals New Possibilities in Matrix Multiplication","url":"https://www.quantamagazine.org/ai-reveals-new-possibilities-in-matrix-multiplication-20221123/","kind":"coverage"}],"url":"https://whataifound.org/finding/2022-10-05-alphatensor"},{"id":"2022-02-16-tokamak-plasma-control","title":"Deep reinforcement learning controls tokamak fusion plasma","claim":"A reinforcement-learning controller learned to shape and stabilise the magnetic confinement of real fusion plasma inside the TCV tokamak, holding configurations that are hard to sustain by hand.","field":"physics","date":"2022-02-16","added":"2026-07-21","lab":"Google DeepMind","model":"DeepMind RL controller","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["physics","fusion","reinforcement-learning","control"],"sources":[{"label":"Nature: Magnetic control of tokamak plasmas through deep reinforcement learning","url":"https://www.nature.com/articles/s41586-021-04301-9","kind":"research"},{"label":"DeepMind: Accelerating fusion science through learned plasma control","url":"https://deepmind.google/discover/blog/accelerating-fusion-science-through-learned-plasma-control/","kind":"announcement"},{"label":"EPFL: EPFL and DeepMind use AI to control plasmas for fusion","url":"https://actu.epfl.ch/news/epfl-and-deepmind-use-ai-to-control-plasmas-for-nu/","kind":"announcement"}],"url":"https://whataifound.org/finding/2022-02-16-tokamak-plasma-control"},{"id":"2021-12-01-knot-theory-intuition","title":"Two theorems found by machine pattern-spotting in knot theory and representation theory","claim":"Networks trained to predict one mathematical invariant from another, then probed for which inputs mattered, pointed mathematicians to a proved theorem linking a knot's signature to a new geometric quantity, and to structure behind the combinatorial invariance conjecture.","field":"mathematics","date":"2021-12-01","added":"2026-07-29","lab":"Google DeepMind (with Oxford and Sydney)","model":"Supervised networks with gradient-based attribution","verification":"peer-reviewed","autonomy":"ai-assisted","tags":["knot-theory","representation-theory","conjecture-generation"],"humans":["Alex Davies","Marc Lackenby","Geordie Williamson"],"sources":[{"label":"Nature: Advancing mathematics by guiding human intuition with AI","url":"https://www.nature.com/articles/s41586-021-04086-x","kind":"research"},{"label":"Knot theory and representation theory notebooks","url":"https://github.com/google-deepmind/mathematics_conjectures","kind":"research"},{"label":"University of Oxford: Machine learning helps mathematicians make new connections","url":"https://www.ox.ac.uk/news/2021-12-01-machine-learning-helps-mathematicians-make-new-connections-0","kind":"announcement"},{"label":"Ernest Davis: Deep Learning and Mathematical Intuition (review)","url":"https://arxiv.org/abs/2112.04324","kind":"challenge"}],"url":"https://whataifound.org/finding/2021-12-01-knot-theory-intuition"},{"id":"2021-07-15-alphafold2","title":"Accurate protein structure prediction across the known proteome (AlphaFold2)","claim":"AlphaFold2 predicted three-dimensional structures for nearly all catalogued proteins from amino-acid sequence at accuracy rivalling experiment, work that earned the 2024 Nobel Prize in Chemistry.","field":"biology","date":"2021-07-15","added":"2026-07-21","lab":"Google DeepMind","model":"AlphaFold2","verification":"independent","autonomy":"ai-led","tags":["protein-structure","biology","alphafold","nobel-prize"],"humans":["John Jumper","Demis Hassabis"],"year_posed":1972,"sources":[{"label":"Nature: Highly accurate protein structure prediction with AlphaFold","url":"https://www.nature.com/articles/s41586-021-03819-2","kind":"research"},{"label":"AlphaFold code (google-deepmind/alphafold)","url":"https://github.com/google-deepmind/alphafold","kind":"research"},{"label":"DeepMind: AlphaFold","url":"https://deepmind.google/science/alphafold/","kind":"announcement"},{"label":"Nobel Prize: Chemistry 2024 press release","url":"https://www.nobelprize.org/prizes/chemistry/2024/press-release/","kind":"commentary"}],"url":"https://whataifound.org/finding/2021-07-15-alphafold2"},{"id":"2021-04-29-wagner-combinatorics","title":"Reinforcement learning refutes several conjectures in extremal combinatorics","claim":"A neural network building graphs edge by edge under a cross-entropy search produced explicit counterexamples to several published conjectures in graph theory and extremal combinatorics.","field":"mathematics","date":"2021-04-29","added":"2026-07-29","lab":"Tel Aviv University","model":"Deep cross-entropy method (custom network)","verification":"independent","autonomy":"search-scaffold","tags":["combinatorics","graph-theory","counterexample","reinforcement-learning"],"humans":["Adam Zsolt Wagner"],"sources":[{"label":"arXiv: Constructions in combinatorics via neural networks","url":"https://arxiv.org/abs/2104.14516","kind":"research"},{"label":"Wagner's cross-entropy code for the counterexamples","url":"https://github.com/zawagner22/cross-entropy-for-combinatorics","kind":"research"},{"label":"Refutation of Spectral Graph Theory Conjectures with Monte Carlo Search","url":"https://arxiv.org/abs/2207.03343","kind":"challenge"}],"url":"https://whataifound.org/finding/2021-04-29-wagner-combinatorics"},{"id":"2020-02-20-halicin","title":"Halicin, an antibiotic found by a neural network screening a compound library","claim":"A graph neural network trained on 2,335 molecules picked halicin out of a repurposing library; it killed multidrug-resistant bacteria including Acinetobacter baumannii and Mycobacterium tuberculosis in vitro and cleared infections in mice.","field":"medicine","date":"2020-02-20","added":"2026-07-29","lab":"MIT / Broad Institute","model":"Directed message-passing graph neural network (Chemprop)","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["antibiotics","drug-repurposing","graph-neural-network"],"humans":["Jonathan Stokes","Regina Barzilay","James Collins"],"sources":[{"label":"Cell: A deep learning approach to antibiotic discovery","url":"https://www.cell.com/cell/fulltext/S0092-8674(20)30102-1","kind":"research"},{"label":"MIT News: Artificial intelligence yields new antibiotic","url":"https://news.mit.edu/2020/artificial-intelligence-identifies-new-antibiotic-0220","kind":"announcement"}],"url":"https://whataifound.org/finding/2020-02-20-halicin"},{"id":"2017-12-14-kepler-90i","title":"An eighth planet around Kepler-90 found by a neural network","claim":"A convolutional network re-examining Kepler light curves recovered transit signals the standard pipeline had ranked below threshold, yielding Kepler-90i and making Kepler-90 the first star besides the Sun known to host eight planets.","field":"astronomy","date":"2017-12-14","added":"2026-07-29","lab":"Google Brain / University of Texas at Austin","model":"Convolutional neural network (AstroNet)","verification":"peer-reviewed","autonomy":"search-scaffold","tags":["exoplanets","kepler","transit-detection"],"humans":["Christopher Shallue","Andrew Vanderburg"],"sources":[{"label":"The Astronomical Journal: Identifying Exoplanets with Deep Learning","url":"https://iopscience.iop.org/article/10.3847/1538-3881/aa9e09","kind":"research"},{"label":"AstroNet: Kepler light-curve models (exoplanet-ml)","url":"https://github.com/google-research/exoplanet-ml","kind":"research"},{"label":"NASA: Artificial intelligence, NASA data used to discover eighth planet circling distant star","url":"https://www.nasa.gov/news-release/artificial-intelligence-nasa-data-used-to-discover-eighth-planet-circling-distant-star/","kind":"announcement"}],"url":"https://whataifound.org/finding/2017-12-14-kepler-90i"}]}