Open review queue

The grade rests on the announcing lab alone.

Better evidenced, still unconfirmed outside the lab.

The year the problem was first posed.

Randomised trial of an AI management platform for breast cancer patients on home CDK4/6 inhibitor therapy Deep learning marker of mortality risk from retinal photographs, validated in three external cohorts (RetiME) Lean formalization of interior gradient Hölder estimates for infinity-harmonic functions Pediatric posterior fossa tumour classifier from T2 MRI with abstention, evaluated at an outside site (PedDx) Smartphone profile photograph screening for skeletal malocclusion, externally validated in Turkey and Belgium Randomised trial of voice-guided AI navigation for biliopancreatic endoscopic ultrasound A shortened CAR intracellular domain designed with Claude Code Claude-generated antibody designs that dislodge receptor-bound IgE Antibody fragment leads optimised with Claude on affinity, stability and aggregation Measurably isomorphic Bernoulli shifts with different base entropies, proved in Lean System-wide AI scribe deployment and clinician documentation time at a 14-hospital health system Classification of Finite Simple Groups formalized in Lean by directed AI agents Deep learning detection and staging of femoral head osteonecrosis on hip x-rays across six Chinese hospitals OpenAI claim of an existence proof for quantum Yang-Mills theory, held by a shepherding committee Non-uniqueness of unforced two-dimensional Euler flows with unbounded integrable vorticity PHP2Shell: two critical PHP remote code execution flaws found with AI assistance Multiagent language-model and CNN system scores BT-RADS on glioma follow-up MRI Chest radiograph model for prescreening reduced ejection fraction, tested in three Korean cohorts Claude-designed protein binders against five scorpion neurotoxins Lean formalization of the L³ bound for the trilinear Hilbert transform ECG deep learning ensemble separates Takotsubo syndrome from anterior STEMI and improves reader accuracy Pointwise convergence of ergodic averages along two commuting transformations Épi agent reports 120 record bounds and constructions, with released certificates NIST elliptic-curve seeds traced to a 1990s C random number generator seeded with the clock LLM-designed quantum circuits with fewer gates and qubits than published designs in seven of eight tasks AI-enhanced auscultation for left ventricular dysfunction, validated in prospective Japanese cohorts RFdiffusion3 designs active phosphotriesterases and transthyretin-specific zinc proteases zero-shot Randomised trial of AI-generated lay summaries before neurosurgical consultations Adapting an adult chest-radiograph model to neonatal intensive care across 30 units No zeros of any Dedekind zeta function with real part above 31/32, machine-checked in Lean Lower bound of 21 multiplications for 3×3 matrix multiplication over every field, with a Lean proof Randomised trial of AI-supported diabetic retinopathy screening in Tanzania Randomised trial of AI wearable monitoring after heart-failure discharge finds no fall in rehospitalisation (LINK-HF2) Pragmatic randomised trial of AI-triggered decision support for postoperative delirium finds no effect AMIE with real patients before urgent primary care visits: a prospective feasibility study Lambert series values, including the Erdős-Borwein constant, are not quadratic irrationals Physicians steered by a covertly adversarial chatbot made harmful decisions at 49% of targeted points, against 2% with an aligned one 719 manuscripts in 372 result families from an unreleased OpenAI model Kakeya maximal conjecture in three dimensions and the Kakeya set conjecture in four Modularity of every elliptic curve over every imaginary quadratic field Negative answer to the hyperinvariant subspace problem on Hilbert space Massive continuum limit of the two-dimensional O(3) model Shelah's eventual categoricity conjecture for abstract elementary classes Optimal packings of one to seven unit squares in a circle, proved in Lean 36 manuscripts across 18 fields from the BootLoops harness run with Claude Six-particle MHV amplitude in planar N=4 super Yang-Mills computed at nine loops Locked AI model for p16/Ki-67 dual-stain triage validated on 9,006 cervical screening cases Agent-run genome survey identifies array-associated reverse transcriptases in jumbo phages Counterexample to Talagrand's operator cotype problem Huang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputs Finite-time blowup for the IPM equation with uniformly space-time smooth forcing Exponential lower bound for the bit pigeonhole principle in unrestricted resolution over parities Eight open problems from Formal Conjectures proved in Lean by a simple agent loop Existence of the core in approval-based committee elections A 3-generator 9-relator group with unsolvable word problem, and smaller Adian-Rabin families Finite-time blowup for the unforced Euler equations from smooth compactly supported data Improved lower bound for the complex Grothendieck constant Disputed claim that Catalan's constant is irrational Randomized metric distortion improved to 2.3282 Lean proof that the percolation probability vanishes at the critical point in every dimension Hyperbolic surfaces with large systoles in every large genus Not every Heyting algebra is the subterminal lattice of a topos Supporting affine functionals for entanglement of formation need not exist Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week Counterexample to Nevanlinna's half-plane omitted-values question Improved algebraic construction for off-diagonal Ramsey numbers Elliptic curves over the rationals of rank at least 30 and at least 31 A smooth random fast dynamo on the three-torus Bounded prime gaps of 246 formalized in Lean from Bombieri-Vinogradov Complete minimizer picture for Gamow's liquid drop model A prescribed Hamiltonian cycle that a book-embedding algorithm cannot produce Proportion of zeta zeros on the critical line raised to 67.25% Huang-Jiang-Oblomkov conjecture for a = 3: a new infinite family of Rogers-Ramanujan identities, with a Lean certificate conditional on eight literature facts Optimal exponent relating sumsets and difference sets determined Sabidussi's compatibility conjecture proved Counterexample to Grothendieck's question on finite flat group schemes Cluster-randomised trial of an LLM decision-support tool in Kenyan primary care finds no reduction in treatment failure First Herculaneum scroll read end to end without unrolling it Two kagome superconductors predicted by machine learning and confirmed in the lab Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs Phase 1 trial of a computationally designed pan-sarbecovirus vaccine An antibiotic designed by reinforcement learning clears an MRSA infection in mice Multicenter prospective validation of Epic's retrained sepsis model (version 2) Randomised trial of AI-supported mammography screening in 105,934 women (MASAI) Inpatient prototype of a conversational EEG device that retrains its own seizure detector Structure in Bruhat intervals of permutation groups Erdős problem #728 resolved and formalized in Lean Randomised trial of two ambient AI scribes in outpatient practice Early science acceleration experiments with GPT-5 AlphaEvolve across 67 problems: 20 improvements, 8 regressions GPT-5 "solved 10 Erdős problems": it located existing solutions Limits to black-box amplification in QMA, with the key step written by GPT-5 New families of unstable singularities in fluid equations AI-generated bacteriophage genomes that replicate and kill bacteria A generative transformer modelling the course of more than 1,000 diseases (Delphi-2M) Strong prime number theorem formalized in Lean by an autoformalization agent Generative medical event models trained on 118 million patients in Epic Cosmos (CoMET, renamed Curiosity) Improved step-size bound in smooth convex optimization Machine-checked Lean proofs for five of six 2025 IMO problems Gold-medal standard at the 2025 International Mathematical Olympiad Phase 2a results for a drug whose target and molecule both came from AI Candidate treatment for dry age-related macular degeneration Randomised comparison of an LLM diagnostic-dialogue system with primary care physicians (AMIE) A fully machine-generated paper passed workshop peer review AI co-scientist hypotheses on antimicrobial resistance and liver fibrosis Enzymes with working catalytic machinery designed from scratch A working fluorescent protein generated by a language model Generative model designs crystals to order; its flagship synthesis turned out to be a known compound Sixty-three previously unrecognised Oracle Bone duplicates found with an image-matching system A neural decoder that identifies quantum errors more accurately than hand-designed methods Complete wiring diagram of an adult fruit-fly brain Zero-shot drug repurposing predictions across 17,080 diseases (TxGNN) Silver-medal standard at the 2024 International Mathematical Olympiad Joint structure prediction for proteins, nucleic acids and ligands (AlphaFold 3) Reinforcement learning steers a tokamak away from tearing instabilities Olympiad geometry solved without human demonstrations A language-model agent that planned and ran chemistry experiments on lab robots A new structural class of antibiotic candidates against MRSA Large-scale prediction of new stable crystalline materials (GNoME) Autonomous laboratory reports solid-state synthesis of new inorganic compounds Medium-range weather forecasts from a graph neural network beat the operational physics model Pathogenicity predictions for 71 million human missense variants Faster sorting routines discovered and merged into the LLVM C++ library Prospective multi-site study of the TREWS sepsis early-warning system Deep reinforcement learning controls tokamak fusion plasma Two theorems found by machine pattern-spotting in knot theory and representation theory Epic Sepsis Model, version 1, disputed by external validation Pragmatic randomised trial of an AI-ECG for low ejection fraction in primary care (EAGLE) Reinforcement learning refutes several conjectures in extremal combinatorics Halicin, an antibiotic found by a neural network screening a compound library Baricitinib for COVID-19, named by a knowledge-graph search and confirmed in randomised trials Pivotal trial of an autonomous AI diagnostic for diabetic retinopathy (IDx-DR) An eighth planet around Kepler-90 found by a neural network

A thread where the result was debated.

Randomised trial of an AI management platform for breast cancer patients on home CDK4/6 inhibitor therapy Deep learning marker of mortality risk from retinal photographs, validated in three external cohorts (RetiME) Lean formalization of interior gradient Hölder estimates for infinity-harmonic functions Pediatric posterior fossa tumour classifier from T2 MRI with abstention, evaluated at an outside site (PedDx) Smartphone profile photograph screening for skeletal malocclusion, externally validated in Turkey and Belgium Randomised trial of voice-guided AI navigation for biliopancreatic endoscopic ultrasound Weak normalization implies strong normalization in pure type systems with βη-conversion, proved in Lean Measurably isomorphic Bernoulli shifts with different base entropies, proved in Lean System-wide AI scribe deployment and clinician documentation time at a 14-hospital health system A subexponential algorithm for counting 3-SAT solutions, refuting the Exponential Time Hypothesis Sogge's local smoothing conjecture claimed in every dimension, with Bochner–Riesz and Kakeya as consequences Deep learning detection and staging of femoral head osteonecrosis on hip x-rays across six Chinese hospitals Non-uniqueness of unforced two-dimensional Euler flows with unbounded integrable vorticity Multiagent language-model and CNN system scores BT-RADS on glioma follow-up MRI Chest radiograph model for prescreening reduced ejection fraction, tested in three Korean cohorts Lean formalization of the L³ bound for the trilinear Hilbert transform Erdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateral Erdős Problem 111: graphs that are not countably colorable need superlinear deletions to become bipartite Erdős Problem 408: an unconditional normal order for the number of totient iterations ECG deep learning ensemble separates Takotsubo syndrome from anterior STEMI and improves reader accuracy Pointwise convergence of ergodic averages along two commuting transformations Épi agent reports 120 record bounds and constructions, with released certificates AI-enhanced auscultation for left ventricular dysfunction, validated in prospective Japanese cohorts RFdiffusion3 designs active phosphotriesterases and transthyretin-specific zinc proteases zero-shot Randomised trial of AI-generated lay summaries before neurosurgical consultations Adapting an adult chest-radiograph model to neonatal intensive care across 30 units No zeros of any Dedekind zeta function with real part above 31/32, machine-checked in Lean Lower bound of 21 multiplications for 3×3 matrix multiplication over every field, with a Lean proof Randomised trial of AI-supported diabetic retinopathy screening in Tanzania Strict Pólya inequalities claimed for simply connected planar domains, Dirichlet and Neumann, with Lean formalizations Randomised trial of AI wearable monitoring after heart-failure discharge finds no fall in rehospitalisation (LINK-HF2) Pragmatic randomised trial of AI-triggered decision support for postoperative delirium finds no effect AMIE with real patients before urgent primary care visits: a prospective feasibility study Lambert series values, including the Erdős-Borwein constant, are not quadratic irrationals Matrix multiplication exponent below 2.3710449, machine-checked over every commutative ring Counterexamples to Zak's modified integer round-down conjecture for the skiving stock problem Physicians steered by a covertly adversarial chatbot made harmful decisions at 49% of targeted points, against 2% with an aligned one Integer multiplication below n log n, against the Schönhage–Strassen optimality conjecture Kannan–Lovász–Simonovits conjecture proved in two preprints posted the same day Closed form for the anisotropic Watson integral of the cubic lattice 36 manuscripts across 18 fields from the BootLoops harness run with Claude Six-task counterexample to the Kernel Conjecture of pinwheel scheduling Erdős Problem #1220 formalized as not provable in ZFC, from a 1987 Shelah-Stanley consistency result Hamilton cycles in connected Cayley graphs of polylogarithmic degree, toward the Lovász conjecture Locked AI model for p16/Ki-67 dual-stain triage validated on 9,006 cervical screening cases Counterexample to Talagrand's operator cotype problem Huang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputs Browning-Sawin conjecture on random sign-coefficient hypersurfaces proved, with a Lean formalization assuming existing literature Four Color Theorem formalized in Lean 4 by AI agents, in two independent developments Finite-time blowup for the IPM equation with uniformly space-time smooth forcing Exponential lower bound for the bit pigeonhole principle in unrestricted resolution over parities Nivat's conjecture claimed in its sharp form, with the submitter stating he cannot check it Eight open problems from Formal Conjectures proved in Lean by a simple agent loop Existence of the core in approval-based committee elections A 3-generator 9-relator group with unsolvable word problem, and smaller Adian-Rabin families Improved lower bound for the complex Grothendieck constant Bollobas-Nikiforov conjecture claimed in full, in a weighted form Disproof of the Ibragimov-Iosifescu conjecture for phi-mixing sequences Lean disproof of Krempa's matrix form of the Koethe conjecture Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement Disputed claim that Catalan's constant is irrational Counterexample to Smale's mean value conjecture at K = 1 Bounded prime gaps improved to 212, with a Lean certificate of the deduction A quantum oracle separating QMA(2) from QMA Confirmation of the Daykin-Frankl conjecture from a language-model proof A smooth counterexample to the Trautman conjecture Entropy production of the Boltzmann equation is not always monotone Common neighbour conjectures for Saxl graphs fail at every base size Counterexample to the stable forking conjecture Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication Criteria and two quadratic instances for Bugeaud's Problem 10.61 Dean's conjecture for k = 5, cycles of length divisible by five Randomized metric distortion improved to 2.3282 Lean proof that the percolation probability vanishes at the critical point in every dimension Hyperbolic surfaces with large systoles in every large genus Not every Heyting algebra is the subterminal lattice of a topos Supporting affine functionals for entanglement of formation need not exist Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week Proof of the Lyons–White conjecture on rate-monotonic random walks Counterexample to Nevanlinna's half-plane omitted-values question Rapid mixing for spin systems on graphs of girth at least five Improved algebraic construction for off-diagonal Ramsey numbers Improved lower bound for large gaps between consecutive primes Sparse domination implies convex body domination Equivalence of generic stability notions for Keisler measures Fröberg's conjecture for quintics and septics in four variables Optimal linear encoding rate for lossy compression of Bernoulli sources Transcendence in the affine case of Erdős Problem 270 Dubickas's question on integral parts of powers of square roots settled Stable commutator length of a relator is not a one-relator group invariant Counterexample to the bounded mass property on the Hopf threefold Marton's inner bound shown not to reach the broadcast channel capacity region A smooth random fast dynamo on the three-torus Counterexamples to the fractional colouring conjecture for Pauli shadow tomography Counterexample to the Yau–Tian–Donaldson conjecture for constant scalar curvature metrics Counterexample to the smooth Carathéodory conjecture on umbilic points First open case of the big-line-big-clique conjecture Counting linear extensions below the 2ⁿ barrier Erdős Problem #501 shown independent of ZFC, with both directions in Lean The DeLaViña-Waller conjecture on the Wiener index Partial proof of the Kasami APN triple-count conjecture, verified in Lean Bounded prime gaps of 246 formalized in Lean from Bombieri-Vinogradov Dimension-free weak-type bound for the vector Riesz transform Matrix multiplication exponent lowered to below 2.371177 Talagrand's convolution conjecture proved on the Boolean hypercube SOP₂ and SOP₃ theories shown to coincide Banach's isometric conjecture settled in the remaining odd dimensions Complete minimizer picture for Gamow's liquid drop model A prescribed Hamiltonian cycle that a book-embedding algorithm cannot produce A 112-vertex counterexample to the Petersen coloring conjecture Separation between the ordinary and strong Kreiss constants Huang-Jiang-Oblomkov conjecture for a = 3: a new infinite family of Rogers-Ramanujan identities, with a Lean certificate conditional on eight literature facts Sendov's conjecture proved for every degree Counterexamples to Schiffer's conjecture and the Pompeiu problem Asymptotic degree-diameter problem resolved for fixed diameter Optimal exponent relating sumsets and difference sets determined Kemeny rank aggregation shown NP-hard for three voters Feige's conjecture on sums of nonnegative random variables settled Counterexamples to the Gaussian moments conjecture Eight problems from the Kourovka Notebook solved and formalized in Lean Gaussian product inequality conjecture proved Counterexample to the Jacobian conjecture in dimension three Near-quadratic lower bound for derivative-free convex optimization Sabidussi's compatibility conjecture proved Cluster-randomised trial of an LLM decision-support tool in Kenyan primary care finds no reduction in treatment failure Two kagome superconductors predicted by machine learning and confirmed in the lab Identity for the critical exponents of jamming derived analytically Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs Phase 1 trial of a computationally designed pan-sarbecovirus vaccine An antibiotic designed by reinforcement learning clears an MRSA infection in mice Multicenter prospective validation of Epic's retrained sepsis model (version 2) Randomised trial of AI-supported mammography screening in 105,934 women (MASAI) Erdős Problem 654 answered negatively by Google DeepMind's Aletheia agent Inpatient prototype of a conversational EEG device that retrains its own seizure detector Erdős problem #728 resolved and formalized in Lean Randomised trial of two ambient AI scribes in outpatient practice Early science acceleration experiments with GPT-5 Limits to black-box amplification in QMA, with the key step written by GPT-5 New families of unstable singularities in fluid equations AI-generated bacteriophage genomes that replicate and kill bacteria A generative transformer modelling the course of more than 1,000 diseases (Delphi-2M) Strong prime number theorem formalized in Lean by an autoformalization agent Generative medical event models trained on 118 million patients in Epic Cosmos (CoMET, renamed Curiosity) Machine-checked Lean proofs for five of six 2025 IMO problems Phase 2a results for a drug whose target and molecule both came from AI Candidate treatment for dry age-related macular degeneration Randomised comparison of an LLM diagnostic-dialogue system with primary care physicians (AMIE) A fully machine-generated paper passed workshop peer review AI co-scientist hypotheses on antimicrobial resistance and liver fibrosis Enzymes with working catalytic machinery designed from scratch Sixty-three previously unrecognised Oracle Bone duplicates found with an image-matching system A neural decoder that identifies quantum errors more accurately than hand-designed methods Complete wiring diagram of an adult fruit-fly brain Zero-shot drug repurposing predictions across 17,080 diseases (TxGNN) A language-model agent that planned and ran chemistry experiments on lab robots A new structural class of antibiotic candidates against MRSA Medium-range weather forecasts from a graph neural network beat the operational physics model Pathogenicity predictions for 71 million human missense variants Prospective multi-site study of the TREWS sepsis early-warning system Two theorems found by machine pattern-spotting in knot theory and representation theory Epic Sepsis Model, version 1, disputed by external validation Pragmatic randomised trial of an AI-ECG for low ejection fraction in primary care (EAGLE) Reinforcement learning refutes several conjectures in extremal combinatorics Baricitinib for COVID-19, named by a knowledge-graph search and confirmed in randomised trials Pivotal trial of an autonomous AI diagnostic for diabetic retinopathy (IDx-DR) An eighth planet around Kepler-90 found by a neural network

Nobody has cited a rebuttal, a critical review, or prior work. An entry with no challenge is not necessarily unchallenged; it may just be unexamined.

Randomised trial of an AI management platform for breast cancer patients on home CDK4/6 inhibitor therapy Deep learning marker of mortality risk from retinal photographs, validated in three external cohorts (RetiME) Lean formalization of interior gradient Hölder estimates for infinity-harmonic functions Pediatric posterior fossa tumour classifier from T2 MRI with abstention, evaluated at an outside site (PedDx) Smartphone profile photograph screening for skeletal malocclusion, externally validated in Turkey and Belgium Randomised trial of voice-guided AI navigation for biliopancreatic endoscopic ultrasound A shortened CAR intracellular domain designed with Claude Code Antibody fragment leads optimised with Claude on affinity, stability and aggregation Weak normalization implies strong normalization in pure type systems with βη-conversion, proved in Lean Measurably isomorphic Bernoulli shifts with different base entropies, proved in Lean System-wide AI scribe deployment and clinician documentation time at a 14-hospital health system A subexponential algorithm for counting 3-SAT solutions, refuting the Exponential Time Hypothesis A subexponential counting algorithm for fixed-width CNF, refuting the Exponential Time Hypothesis Classification of Finite Simple Groups formalized in Lean by directed AI agents Sogge's local smoothing conjecture claimed in every dimension, with Bochner–Riesz and Kakeya as consequences Deep learning detection and staging of femoral head osteonecrosis on hip x-rays across six Chinese hospitals OpenAI claim of an existence proof for quantum Yang-Mills theory, held by a shepherding committee Non-uniqueness of unforced two-dimensional Euler flows with unbounded integrable vorticity PHP2Shell: two critical PHP remote code execution flaws found with AI assistance Multiagent language-model and CNN system scores BT-RADS on glioma follow-up MRI Chest radiograph model for prescreening reduced ejection fraction, tested in three Korean cohorts Claude-designed protein binders against five scorpion neurotoxins Lean formalization of the L³ bound for the trilinear Hilbert transform Erdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateral Erdős Problem 111: graphs that are not countably colorable need superlinear deletions to become bipartite Erdős Problem 408: an unconditional normal order for the number of totient iterations ECG deep learning ensemble separates Takotsubo syndrome from anterior STEMI and improves reader accuracy Pointwise convergence of ergodic averages along two commuting transformations Épi agent reports 120 record bounds and constructions, with released certificates NIST elliptic-curve seeds traced to a 1990s C random number generator seeded with the clock LLM-designed quantum circuits with fewer gates and qubits than published designs in seven of eight tasks AI-enhanced auscultation for left ventricular dysfunction, validated in prospective Japanese cohorts RFdiffusion3 designs active phosphotriesterases and transthyretin-specific zinc proteases zero-shot Randomised trial of AI-generated lay summaries before neurosurgical consultations Adapting an adult chest-radiograph model to neonatal intensive care across 30 units No zeros of any Dedekind zeta function with real part above 31/32, machine-checked in Lean Lower bound of 21 multiplications for 3×3 matrix multiplication over every field, with a Lean proof Randomised trial of AI-supported diabetic retinopathy screening in Tanzania Strict Pólya inequalities claimed for simply connected planar domains, Dirichlet and Neumann, with Lean formalizations Randomised trial of AI wearable monitoring after heart-failure discharge finds no fall in rehospitalisation (LINK-HF2) Pragmatic randomised trial of AI-triggered decision support for postoperative delirium finds no effect AMIE with real patients before urgent primary care visits: a prospective feasibility study Lambert series values, including the Erdős-Borwein constant, are not quadratic irrationals Matrix multiplication exponent below 2.3710449, machine-checked over every commutative ring Counterexamples to Zak's modified integer round-down conjecture for the skiving stock problem Physicians steered by a covertly adversarial chatbot made harmful decisions at 49% of targeted points, against 2% with an aligned one 719 manuscripts in 372 result families from an unreleased OpenAI model Quasi-Riemann hypothesis: no zeros of zeta or any Dirichlet L-function with real part above 7/8 Kakeya maximal conjecture in three dimensions and the Kakeya set conjecture in four Counterexample to the Borel conjecture in dimension four Artin's primitive root conjecture: infinitely many primes for every admissible base Modularity of every elliptic curve over every imaginary quadratic field Negative answer to the hyperinvariant subspace problem on Hilbert space Massive continuum limit of the two-dimensional O(3) model Proof of Barnette's conjecture on Hamiltonian cycles in cubic bipartite planar graphs Matrix multiplication exponent bounded by 9/4 Integer multiplication below n log n, against the Schönhage–Strassen optimality conjecture Truly subquadratic 3SUM and truly subcubic APSP, refuting two central fine-grained complexity hypotheses Kannan–Lovász–Simonovits conjecture proved in two preprints posted the same day Optimal packings of one to seven unit squares in a circle, proved in Lean Closed form for the anisotropic Watson integral of the cubic lattice 36 manuscripts across 18 fields from the BootLoops harness run with Claude Six-task counterexample to the Kernel Conjecture of pinwheel scheduling Erdős Problem #1220 formalized as not provable in ZFC, from a 1987 Shelah-Stanley consistency result Hamilton cycles in connected Cayley graphs of polylogarithmic degree, toward the Lovász conjecture Six-particle MHV amplitude in planar N=4 super Yang-Mills computed at nine loops Locked AI model for p16/Ki-67 dual-stain triage validated on 9,006 cervical screening cases Agent-run genome survey identifies array-associated reverse transcriptases in jumbo phages Counterexample to Talagrand's operator cotype problem Huang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputs Browning-Sawin conjecture on random sign-coefficient hypersurfaces proved, with a Lean formalization assuming existing literature Four Color Theorem formalized in Lean 4 by AI agents, in two independent developments Finite-time blowup for the IPM equation with uniformly space-time smooth forcing Exponential lower bound for the bit pigeonhole principle in unrestricted resolution over parities Nivat's conjecture claimed in its sharp form, with the submitter stating he cannot check it Eight open problems from Formal Conjectures proved in Lean by a simple agent loop Existence of the core in approval-based committee elections A 3-generator 9-relator group with unsolvable word problem, and smaller Adian-Rabin families Finite-time blowup for the unforced Euler equations from smooth compactly supported data Improved lower bound for the complex Grothendieck constant Bollobas-Nikiforov conjecture claimed in full, in a weighted form Disproof of the Ibragimov-Iosifescu conjecture for phi-mixing sequences Fermat's Last Theorem formalized end to end in Lean 4 Lean disproof of Krempa's matrix form of the Koethe conjecture Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement Counterexample to Smale's mean value conjecture at K = 1 Bounded prime gaps improved to 212, with a Lean certificate of the deduction A quantum oracle separating QMA(2) from QMA Confirmation of the Daykin-Frankl conjecture from a language-model proof A smooth counterexample to the Trautman conjecture Prime gaps at most 186, conditional on three unproved Lean axioms Entropy production of the Boltzmann equation is not always monotone Common neighbour conjectures for Saxl graphs fail at every base size Counterexample to the stable forking conjecture Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication Criteria and two quadratic instances for Bugeaud's Problem 10.61 Dean's conjecture for k = 5, cycles of length divisible by five Randomized metric distortion improved to 2.3282 Lean proof that the percolation probability vanishes at the critical point in every dimension Hyperbolic surfaces with large systoles in every large genus Not every Heyting algebra is the subterminal lattice of a topos Supporting affine functionals for entanglement of formation need not exist Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week Proof of the Lyons–White conjecture on rate-monotonic random walks Counterexample to Nevanlinna's half-plane omitted-values question Rapid mixing for spin systems on graphs of girth at least five Improved algebraic construction for off-diagonal Ramsey numbers Improved lower bound for large gaps between consecutive primes Sparse domination implies convex body domination Equivalence of generic stability notions for Keisler measures Fröberg's conjecture for quintics and septics in four variables Optimal linear encoding rate for lossy compression of Bernoulli sources A complex structure on the six-sphere Elliptic curves over the rationals of rank at least 30 and at least 31 Transcendence in the affine case of Erdős Problem 270 Dubickas's question on integral parts of powers of square roots settled Stable commutator length of a relator is not a one-relator group invariant Counterexample to the bounded mass property on the Hopf threefold Marton's inner bound shown not to reach the broadcast channel capacity region A smooth random fast dynamo on the three-torus Counterexamples to the fractional colouring conjecture for Pauli shadow tomography Counterexample to the Yau–Tian–Donaldson conjecture for constant scalar curvature metrics Counterexample to the smooth Carathéodory conjecture on umbilic points First open case of the big-line-big-clique conjecture Counting linear extensions below the 2ⁿ barrier Erdős Problem #501 shown independent of ZFC, with both directions in Lean The DeLaViña-Waller conjecture on the Wiener index Partial proof of the Kasami APN triple-count conjecture, verified in Lean Bounded prime gaps of 246 formalized in Lean from Bombieri-Vinogradov Dimension-free weak-type bound for the vector Riesz transform Matrix multiplication exponent lowered to below 2.371177 Talagrand's convolution conjecture proved on the Boolean hypercube SOP₂ and SOP₃ theories shown to coincide Banach's isometric conjecture settled in the remaining odd dimensions Complete minimizer picture for Gamow's liquid drop model A prescribed Hamiltonian cycle that a book-embedding algorithm cannot produce Proportion of zeta zeros on the critical line raised to 67.25% A 112-vertex counterexample to the Petersen coloring conjecture Separation between the ordinary and strong Kreiss constants Huang-Jiang-Oblomkov conjecture for a = 3: a new infinite family of Rogers-Ramanujan identities, with a Lean certificate conditional on eight literature facts Sendov's conjecture proved for every degree Counterexamples to Schiffer's conjecture and the Pompeiu problem Asymptotic degree-diameter problem resolved for fixed diameter Optimal exponent relating sumsets and difference sets determined Kemeny rank aggregation shown NP-hard for three voters Feige's conjecture on sums of nonnegative random variables settled Counterexample to the Dinitz–Garg–Goemans conjecture Counterexamples to the Gaussian moments conjecture Eight problems from the Kourovka Notebook solved and formalized in Lean Gaussian product inequality conjecture proved Near-quadratic lower bound for derivative-free convex optimization Sabidussi's compatibility conjecture proved Counterexample to Grothendieck's question on finite flat group schemes Cycle double cover conjecture proved for all bridgeless multigraphs Cluster-randomised trial of an LLM decision-support tool in Kenyan primary care finds no reduction in treatment failure First Herculaneum scroll read end to end without unrolling it Two kagome superconductors predicted by machine learning and confirmed in the lab Identity for the critical exponents of jamming derived analytically Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs Disproof of the Erdős unit-distance conjecture Phase 1 trial of a computationally designed pan-sarbecovirus vaccine An antibiotic designed by reinforcement learning clears an MRSA infection in mice Multicenter prospective validation of Epic's retrained sepsis model (version 2) Randomised trial of AI-supported mammography screening in 105,934 women (MASAI) Erdős Problem 654 answered negatively by Google DeepMind's Aletheia agent Inpatient prototype of a conversational EEG device that retrains its own seizure detector Structure in Bruhat intervals of permutation groups Erdős problem #728 resolved and formalized in Lean Randomised trial of two ambient AI scribes in outpatient practice Early science acceleration experiments with GPT-5 AlphaEvolve across 67 problems: 20 improvements, 8 regressions Limits to black-box amplification in QMA, with the key step written by GPT-5 New families of unstable singularities in fluid equations AI-generated bacteriophage genomes that replicate and kill bacteria A generative transformer modelling the course of more than 1,000 diseases (Delphi-2M) Strong prime number theorem formalized in Lean by an autoformalization agent Generative medical event models trained on 118 million patients in Epic Cosmos (CoMET, renamed Curiosity) Machine-checked Lean proofs for five of six 2025 IMO problems Gold-medal standard at the 2025 International Mathematical Olympiad Phase 2a results for a drug whose target and molecule both came from AI 4×4 complex matrix multiplication in 48 scalar multiplications Improved lower bound for the 11-dimensional kissing number Improved bound for the Erdős minimum-overlap problem Candidate treatment for dry age-related macular degeneration Randomised comparison of an LLM diagnostic-dialogue system with primary care physicians (AMIE) AI co-scientist hypotheses on antimicrobial resistance and liver fibrosis Enzymes with working catalytic machinery designed from scratch A working fluorescent protein generated by a language model Sixty-three previously unrecognised Oracle Bone duplicates found with an image-matching system A neural decoder that identifies quantum errors more accurately than hand-designed methods Complete wiring diagram of an adult fruit-fly brain Zero-shot drug repurposing predictions across 17,080 diseases (TxGNN) Silver-medal standard at the 2024 International Mathematical Olympiad Reinforcement learning steers a tokamak away from tearing instabilities A language-model agent that planned and ran chemistry experiments on lab robots A new structural class of antibiotic candidates against MRSA New lower bound constructions for the cap set problem Improved heuristics for online bin packing Medium-range weather forecasts from a graph neural network beat the operational physics model Pathogenicity predictions for 71 million human missense variants Faster sorting routines discovered and merged into the LLVM C++ library Faster matrix-multiplication algorithms found by reinforcement learning Prospective multi-site study of the TREWS sepsis early-warning system Deep reinforcement learning controls tokamak fusion plasma Accurate protein structure prediction across the known proteome (AlphaFold2) Pragmatic randomised trial of an AI-ECG for low ejection fraction in primary care (EAGLE) Halicin, an antibiotic found by a neural network screening a compound library Baricitinib for COVID-19, named by a knowledge-graph search and confirmed in randomised trials Pivotal trial of an autonomous AI diagnostic for diabetic retinopathy (IDx-DR) An eighth planet around Kepler-90 found by a neural network