Improved boundNumber theory
Bounded gaps between consecutive primes
A paper proves an upper bound of 212. The Lean certificate verifies a deduction from stated distribution estimates and other analytic inputs.
LFCR
Frontier
New proofs, counterexamples, bounds and formalizations reported by people and AI systems, newest first.
September 2026 11
CounterexampleOther2026-09-03-smale-mean-value-k1
Counterexample to Smale's mean value conjecture at K = 1
GitHub: tadamcz/mean-value-problem, the Lean 4 disproof
LFCR
New proofOther2026-09-03-koethe-conjecture-matrix-form
Lean disproof of Krempa's matrix form of the Koethe conjecture
GitHub: tadamcz/koethe, Lean disproof and Palomar submission repository
LFCR
New proofCombinatorics2026-09-03-erdos-sos-conjecture
Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement
GitHub: tadamcz/erdos548, Lean proof and Palomar submission repository
LFCR
New proofNumber theory2026-09-03-catalan-constant-irrationality
Disputed claim that Catalan's constant is irrational
arXiv: Catalan's constant is irrational
LFCR
CounterexampleOther2026-09-02-trautman-conjecture
A smooth counterexample to the Trautman conjecture
arXiv: A Smooth Counterexample to the Trautman Conjecture
LFCR
New proofTheoretical computer science2026-09-02-qma2-oracle-separation
A quantum oracle separating QMA(2) from QMA
arXiv: A quantum oracle separation between QMA(2) and QMA
LFCR
New proofNumber theory2026-09-02-prime-gaps-186
Prime gaps at most 186, conditional on three unproved Lean axioms
GitHub: openai/PrimeGaps186, the conditional Lean formalization and numerical certificate
LFCR
New proofOther2026-09-02-daykin-frankl-conjecture
Confirmation of the Daykin-Frankl conjecture from a language-model proof
arXiv: Confirmation of the Daykin-Frankl conjecture
LFCR
New proofCombinatorics2026-09-01-saxl-common-neighbour
Common neighbour conjectures for Saxl graphs fail at every base size
arXiv: common neighbour conjectures for Saxl graphs fail at every base size
LFCR
New proofOther2026-09-01-mckean-entropy-production
Entropy production of the Boltzmann equation is not always monotone
arXiv: the entropy production is not always monotone for hard spheres or for Maxwell molecules
LFCR
August 2026 29
CounterexampleOther2026-08-31-stable-forking
Counterexample to the stable forking conjecture
arXiv: a counterexample to the stable forking conjecture
LFCR
New proofOther2026-08-31-pisot-cantor-equidistribution
Criteria and two quadratic instances for Bugeaud's Problem 10.61
GitHub: Pisot-Cantor-61, paper and Lean development
LFCR
New proofTheoretical computer science2026-08-31-boolean-multiplicative-complexity-mul4
Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication
arXiv: unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication
LFCR
New proofTheoretical computer science2026-08-29-metric-distortion-23282
Randomized metric distortion improved to 2.3282
arXiv: improving randomized metric distortion to 2.3282
LFCR
New proofOther2026-08-29-dean-conjecture-k5
Dean's conjecture for k = 5, cycles of length divisible by five
Zenodo: cycles of length divisible by five in graphs of minimum degree five
LFCR
New proofProbability2026-08-28-percolation-critical-point
Lean proof that the percolation probability vanishes at the critical point in every dimension
GitHub: anthropics/formal-math, percolation project at the pinned commit 795efb86
LFCR
New proofAnalysis2026-08-27-norm-variation-ergodic-averages-lean
Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week
arXiv: A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations
LFCR
New proofProbability2026-08-27-lyons-white-conjecture
Proof of the Lyons–White conjecture on rate-monotonic random walks
arXiv: Proof of the Lyons–White Conjecture
LFCR
New proofOther2026-08-27-large-systoles
Hyperbolic surfaces with large systoles in every large genus
arXiv: a note on surfaces with large systoles
LFCR
New proofAlgebra2026-08-27-intuitionistic-higher-order-truth
Not every Heyting algebra is the subterminal lattice of a topos
arXiv: failure of higher-order truth within intuitionistic propositional logic
LFCR
New proofTheoretical computer science2026-08-26-spin-systems-girth-five
Rapid mixing for spin systems on graphs of girth at least five
arXiv: a spectral local-to-global principle for spin systems on graphs with girth at least five
LFCR
CounterexampleOther2026-08-26-nevanlinna-half-plane
Counterexample to Nevanlinna's half-plane omitted-values question
arXiv: Three omitted values and non-Blaschke point divisors in half-planes
LFCR
New proofGeometry and topology2026-08-25-sparse-convex-body-domination
Sparse domination implies convex body domination
arXiv: sparse domination implies convex body domination
LFCR
New proofCombinatorics2026-08-25-ramsey-algebraic-construction
Improved algebraic construction for off-diagonal Ramsey numbers
arXiv: An improved algebraic construction for Ramsey numbers
LFCR
New proofOther2026-08-25-generically-stable-keisler
Equivalence of generic stability notions for Keisler measures
arXiv: generically stable Keisler measures
LFCR
New proofOther2026-08-25-froberg-quintics-septics
Fröberg's conjecture for quintics and septics in four variables
arXiv: Fröberg's conjecture for quintics and septics in four variables
LFCR
Improved boundNumber theory2026-08-25-erdos-4-prime-gaps
Improved lower bound for large gaps between consecutive primes
Manuscript: Erdős_4_GPT_5.6_Sol.pdf
LFCR
New proofTheoretical computer science2026-08-24-ancheta-massey-linear-coding
Optimal linear encoding rate for lossy compression of Bernoulli sources
arXiv: entropy of Bernoulli measures conditioned on affine subspaces and a problem of Ancheta-Massey
LFCR
New proofAnalysis2026-08-23-s6-complex-structure
A complex structure on the six-sphere
Alpöge: The (3,4,infinity) modular family of 2-tori is a complex structure on S⁶ (PDF)
LFCR
New proofOther2026-08-23-elliptic-rank-31
Elliptic curves over the rationals of rank at least 30 and at least 31
Elliptic curve rank leaderboard: curve 302, rank at least 31
LFCR
New proofNumber theory2026-08-22-erdos-270-affine-transcendence
Transcendence in the affine case of Erdős Problem 270
GitHub: algebraic independence in the affine case of Erdős Problem 270
LFCR
New proofAlgebra2026-08-21-scl-relator-invariance
Stable commutator length of a relator is not a one-relator group invariant
arXiv: the stable commutator length of a relator is not a one-relator group invariant
LFCR
New proofOther2026-08-21-dubickas-square-roots
Dubickas's question on integral parts of powers of square roots settled
Even integral parts of powers of square roots (ResearchGate)
LFCR
CounterexampleOther2026-08-21-bounded-mass-property
Counterexample to the bounded mass property on the Hopf threefold
arXiv: a counterexample to the bounded mass property
LFCR
Improved boundTheoretical computer science2026-08-20-marton-inner-bound
Marton's inner bound shown not to reach the broadcast channel capacity region
arXiv: Sub-optimality of Marton's Inner Bound for the Two-Receiver Broadcast Channel
LFCR
New proofProbability2026-08-20-fast-dynamo-three-torus
A smooth random fast dynamo on the three-torus
arXiv: an AI-discovered smooth random fast dynamo on T³
LFCR
CounterexampleOther2026-08-19-yau-tian-donaldson
Counterexample to the Yau–Tian–Donaldson conjecture for constant scalar curvature metrics
arXiv: Disproof of the Yau–Tian–Donaldson conjecture
LFCR
New proofTheoretical computer science2026-08-19-linear-extensions-below-2n
Counting linear extensions below the 2ⁿ barrier
arXiv: breaking the 2ⁿ barrier for counting linear extensions with a short elementary algorithm
LFCR
New proofOther2026-08-19-kasami-apn-triple-counts
Partial proof of the Kasami APN triple-count conjecture, verified in Lean
arXiv: on a conjecture on the Kasami APN function
LFCR