Tracked problems: 670; 465 fully resolved · 1 under review
Combined years open: 9,164; before AI closed them
Lean-verified: 139; machine-checked
Community members: 366; 4 verified · 260 votes · 66 comments

Latest activity

Edits, submissions and discussion · all members

Rasmus Lindahl approved A 32-leaf tree requiring six coordinates for an isometric $\ell_\infty$ embedding3 hours ago
Rasmus Lindahl approved Cycle-residue stability at minimum degree five3 hours ago
Rasmus Lindahl approved Köthe Conjecture3 hours ago
Rasmus Lindahl approved Smale’s Mean Value Conjecture ( $K=1$ )3 hours ago
Rasmus Lindahl approved The proper hat-guessing number of $K_8-e$ 3 hours ago
Rasmus Lindahl approved The proper hat-guessing number of $K_7-e$ 3 hours ago
BoldJackal580 submitted A 32-leaf tree requiring six coordinates for an isometric $\ell_\infty$ embedding4 hours ago
Matthew Protti submitted The proper hat-guessing number of $K_8-e$ 16 hours ago
eli submitted Cycle-residue stability at minimum degree five17 hours ago
HiddenPanther509 changed the what was actually shown and 2 other fields on Equivalence of generic stability notions for Keisler measures to “Let T be a complete first-order theory in discrete or contin…”20 hours ago

Latest

Most recent results

This week

Most significant of the last seven days

All entries

Sort by

Period

all 670 entries

Cycle-residue stability at minimum degree five

ProvedUnder reviewAI co-developed

(The preprint claims an exact classification. Write C_5(G) for the residues modulo five represented by cycle lengths in G. Let E_5=K_6,K_5,5_5,n;t:2≤ t5<n, where H_5,n;t is obtained from K_5,n by deleting 5-t edges incident with one vertex in the part of size n. For every finite simple graph G with minimum degree at least five, exactly one alternative holds: C_5(G)= Z_5; or every end-block belongs to E_5 and every non-end-block contains no cycle of length congruent to two modulo five. Every member of E_5 has cycle-residue spectrum 0,1,3,4. The proof combines structural arguments with finite computational checks. It uses the separately established Dean–5 theorem and its weak-graph strengthening as inputs. The contribution is the stronger stability classification; independent expert review remains pending.)

Graph Theory

Classify the finite simple graphs of minimum degree at least five whose cycle lengths fail to represent every residue class modulo five. Is residue two the only possible missing residue, and can all such graphs be characterized through an explicit family of exceptional end-blocks together with a condition on the remaining blocks?

Posed by Luo, Ma and Zhao, whose stability theorem covers every k >= 6 and leaves k = 5, 2026Open 0yModel GPT-5.6 Sol, GPT-6 Astra (OpenAI)Solved 2026-09-04

PreprintSignificance 20 Submitted by eli on 4 Sep 2026

The proper hat-guessing number of $K_8-e$

ProvedUnder reviewAI co-developed

(We prove HG_P(K_8-e)=14 using an explicit PGL(2,13)-equivariant strategy. A compact formula fixes 990 normalized twin decisions, and a 48,510-edge residual-orbit matching induces consistent rules on 53,460 labelled clique-view orbits. Independent implementations regenerate the certificate and check all 138,378,240 proper fourteen-colourings with zero failures. Unlike the n=5,6,7 constructions, residual right degrees reach eight, so the explicit global matching is load-bearing. A separately labelled companion exhibits one fixed clique completion compatible with 2^380 equivariant twin-rule pairs and proves 380 optimal within the stated independent whole-tail reversal model; that companion's independent review is pending. The release does not solve the general K_n-e family or K_9-e.)

Graph theory; hat-guessing games; finite geometry; matching theory

Determine the exact proper hat-guessing number of the complete graph on eight vertices with one edge removed. The general bounds leave $\mathrm{HG}_P(K_8-e)\in\{13,14\}$ .

Posed by Adriaensen et al., 2026Open 0yModel GPT-5.6 Pro (OpenAI)Solved 2026-09-04

AnnouncedSignificance 7 Submitted by Matthew Protti on 4 Sep 2026

Improved maximal prime-gap lower bound

ProvedPartialAI-discovered

(The paper proves G(X)≫ log X (log_2 X)^2 log_4 X/(log_3 X)^2 for all sufficiently large X. Its main new ingredient is a short-translates theorem: for any sufficiently small set S⊆[1,H] with |S|≤δ x, one can find a short translate making every corresponding linear form composite. Combining this with an Erdős--Rankin covering argument produces prime-free intervals of the claimed length. This directly and asymptotically improves the August 2026 GPT-5.6 Sol bound G(X)≫log Xlog_2 X/log_4 X by the unbounded factor log_2 X(log_4 X)^2/(log_3 X)^2.)

Analytic number theory

Let $G(X)$ denote the largest gap between consecutive primes not exceeding $X$ , and let $\log_j$ denote the $j$ -fold iterated logarithm. The paper proves that, for all sufficiently large $X$ , $G(X)\gg \frac{\log X\,(\log_2 X)^2\,\log_4 X}{(\log_3 X)^2}.$ Equivalently, there is an absolute constant $c>0$ such that $G(X)$ is at least $c$ times the quantity above for all sufficiently large $X$ . This improves Rankin's classical lower bound by a factor of $\log_2 X$ .

Posed by Paul Erdős, 1955Open 71yModel GPT 6 Astra (OpenAI)Solved 2026-09-03

Site-confirmedSignificance 60 Submitted by VibeGene on 4 Sep 2026

The proper hat-guessing number of $K_7-e$

ProvedUnder reviewAI co-developed

(We prove HG_P(K_7-e)=12. One lower-bound proof uses two explicit block-disjoint S(5,6,12) Witt designs. A second uses orbit maps from an explicitly regenerated sharply five-transitive twelve-point permutation group, combining one set-symmetric and one order-sensitive rule. Both satisfy a general coordinate-line twin-completion criterion, and Hall's theorem completes the clique strategy. The release also proves a disjoint completion-design theorem, an even-n obstruction scoped to set-symmetric line-permutation twins in this sufficient framework, and a prime-admissibility theorem for the design parameters. It does not solve the general K_n-e problem or K_8-e.)

Graph theory; hat-guessing games; Steiner systems; permutation groups

Determine the exact proper hat-guessing number of the complete graph on seven vertices with one edge removed. The general bounds leave $\mathrm{HG}_P(K_7-e)\in\{11,12\}$ .

Posed by Adriaensen et al., 2026Open 0yModel GPT-5.6 Pro (OpenAI)Solved 2026-09-03

AnnouncedSignificance 7 Submitted by Matthew Protti on 4 Sep 2026

Prime Gaps at Most 186

ProvedPartialAI-discovered

(Assuming three explicit input statements, the project proves DHL[40,2]: every admissible 40-tuple contains at least two primes infinitely often after translation. An explicit admissible 40-tuple of diameter 186 then gives _n→∞(p_n+1-p_n)186. The Lean proof of the implication from the three inputs to the final theorem is kernel-checked. Two inputs are Kloosterman-type estimates cited to Katz/Deligne and Fouvry--Kowalski--Michel; the third consists of finitely many numerical integral and cap inequalities backed by a Python/FLINT certificate.)

Analytic number theory

For the sequence of primes $p_n$ , the project derives $\liminf_{n\to\infty}(p_{n+1}-p_n)\le186.$ More precisely, assuming three explicit analytic/numerical inputs, it proves $\mathrm{DHL}[40,2]$ : every admissible set of forty integer shifts has infinitely many translates containing at least two primes. Applying this to an explicit admissible $40$ -tuple of diameter $186$ yields infinitely many consecutive prime gaps of size at most $186$ . The Lean development verifies the deduction from the stated inputs; the two Kloosterman-type estimates and the finite physical-integral/cap bounds remain external assumptions.

Posed by Alphonse de Polignac (the twin prime conjecture); the bounded form since Goldston, Pintz and Yıldırım, 1849Open 177yModel GPT 6 Astra (OpenAI)Solved 2026-09-03

Lean-checked, statement unauditedSignificance 62 Submitted by VibeGene on 3 Sep 2026

Smale’s Mean Value Conjecture ( $K=1$ )

DisprovedUnder reviewAI-discovered

(The formal proof constructs a complex polynomial p such that p(0)=0, p'(0)=1, and for every critical point c of p, |p(c)/c|>1. Thus at z=0 there is no critical point satisfying |p(0)-p(c)|/|c|≤ |p'(0)|=1, which disproves Smale's conjectured universal constant K=1. The counterexample has very large unspecified degree and violates the bound only by a small margin, so it is consistent with Smale's original K=4 theorem, the known low-degree positive cases, and previous asymptotic improvements toward 1.)

Complex polynomials

Smale conjectured that in his mean value theorem for complex polynomials, the universal constant $4$ could be replaced by $1$ . Equivalently, for every complex polynomial $p$ of degree at least $2$ and every $z\in\mathbb C$ , there should exist a critical point $c$ of $p$ such that $\frac{|p(z)-p(c)|}{|z-c|}\le |p'(z)|.$ The conjecture is false: there exists a polynomial $p$ with $p(0)=0$ and $p'(0)=1$ such that $\left|\frac{p(c)}{c}\right|>1$ for every critical point $c$ .

Posed by Stephen Smale, 1981Open 45yModel GPT-6 Astra (pre-release) (OpenAI)Solved 2026-09-03

Lean-verifiedSignificance 45 Submitted by VibeGene on 4 Sep 2026

The proper hat-guessing number of $K_6-e$

ProvedUnder reviewAI co-developed

(We prove HG_P(K_6-e)=10. The lower bound uses two order-sensitive twin-player rules obtained by deleting and repairing one point of an explicit sharply four-transitive eleven-point permutation group. On every coordinate line the repaired rules are derangement permutations, are pointwise unequal, and have fixed-point-free composition. Hall's theorem completes the strategy on the four clique vertices. The release also classifies all repairable orbit labels and proves an even-n obstruction for set-symmetric line-permutation twin rules. It does not solve the general K_n-e family.)

Graph theory; hat-guessing games; permutation groups

Determine the exact proper hat-guessing number of the complete graph on six vertices with one edge removed. The known general bounds leave $\mathrm{HG}_P(K_6-e)\in\{9,10\}$ .

Posed by Adriaensen et al., 2026Open 0yModel GPT-5.6 Pro (OpenAI)Solved 2026-09-03

AnnouncedSignificance 7 Submitted by Matthew Protti on 4 Sep 2026

Conway's Refinement Conjecture for Omnific Integers

ProvedUnder reviewAI co-developed

(The repository gives a Lean proof of Conway's 1976 refinement conjecture for omnific integers: whenever ab=cd with a,b,c,d∈, there exist e,f,g,h∈ satisfying a=ef, b=gh, c=eg, d=fh. The proof is formalized twice: once using CombinatorialGames' surreal-number implementation and once with the required surreal definitions inlined over Mathlib. The development also proves stronger structural results about factorization in Hahn-series integer parts and related generalized power-series rings.)

Surreal numbers

If $a,b,c,d\in\mathbf{Oz}$ are omnific integers and $ab=cd,$ then there exist omnific integers $e,f,g,h\in\mathbf{Oz}$ such that $a=ef,\qquad b=gh,\qquad c=eg,\qquad d=fh.$ Equivalently, every equality of two products in the omnific integers admits a common four-factor refinement.

Posed by John H. Conway, 1976Open 50yModel ChatGPT; Claude (OpenAI; Anthropic)Solved 2026-09-03

Site-confirmedSignificance 28 Submitted by VibeGene on 4 Sep 2026

Köthe Conjecture

DisprovedUnder reviewAI-discovered

(GPT-6 Astra constructs a unital algebra R=k A over the countable field k= F_2, with I=A a nil two-sided ideal, together with a matrix W∈ M_2(I) that is not nilpotent. The algebra A is generated by three weighted backward shifts. A diagonal construction chooses the weights so that every element of A is nilpotent. At the same time, a suitable polynomial combination of the shifts fixes a nonzero vector; this yields a companion-type matrix with a nonzero eigenvalue, and hence a nonnilpotent matrix whose entries lie in I. This formally disproves Krempa's matrix formulation of Köthe's conjecture.)

Noncommutative ring theory

Köthe's conjecture asks whether the sum of two nil left ideals of a ring is always nil. Equivalently, by Krempa's 1972 formulation, if $I$ is a nil two-sided ideal of a ring $R$ , then the matrix ideal $M_n(I)$ should be nil for every finite $n$ , already for $n=2$ .

The conjecture is false: there exists a ring $R$ , a nil two-sided ideal $I\subseteq R$ , and a $2\times 2$ matrix with entries in $I$ that is not nilpotent.

Posed by Gottfried Köthe, 1930Open 96yModel GPT-6 Astra (pre-release) (OpenAI)Solved 2026-09-03

Lean-verifiedSignificance 60 Submitted by VibeGene on 4 Sep 2026

A new bound for small gaps between primes: $H_1 \le 212$

ProvedPartialAI-assisted

(H_1 ≤ 212, improving Stadlmann's 240 of three days earlier and the 246 of Polymath8b that had stood since 2014. The twin prime conjecture, H_1 = 2, is untouched. Held the record for hours at most: OpenAI's paper claiming 186 is dated 30 August, four days before this one, though its Lean development appeared on 2 September.)

Analytic number theory

Write $H_1 = \liminf_{n\to\infty}(p_{n+1}-p_n)$ . Stadlmann had recently proved $H_1 \le 240$ , improving the bound $246$ of Polymath8b. Building on her work, this paper proves $H_1 \le 212$ : infinitely many pairs of consecutive primes are at most $212$ apart.

Posed by Alphonse de Polignac (the twin prime conjecture); the bounded form since Goldston, Pintz and Yıldırım, 1849Open 177yModel AxiomProver (Axiom Math)Solved 2026-09-03

Lean-checked, statement unauditedSignificance 62

Logarithmic basis number of graphs

ProvedAI co-developed

(Knauer proves that every finite n-vertex multigraph satisfies bn(G)=O(log n), improving the previous general O(log^2 n) bound and matching the known Ω(log n) order. He also proves the sharper cycle-rank bound bn(G)=O(logβ(G)). Combined with a reduction of Lehner and Miraftab, this yields bn(G)=O(log g) for graphs of Euler genus g, improving the previous O(log^2 g) bound to the optimal logarithmic order.)

Graph theory

The basis number $\mathrm{bn}(G)$ of a graph $G$ is the minimum edge-congestion of a basis of its cycle space. We prove that every finite $n$ -vertex multigraph satisfies $\mathrm{bn}(G)=O(\log n),$ resolving, for simple graphs, a question of Bazargani, Biedl, Bose, Maheshwari and Miraftab, subsequently stated as a conjecture by Miraftab, Morin and Yuditsky. The argument also yields the cycle-rank refinement $\mathrm{bn}(G)=O(\log \beta(G)),$ where $\beta(G)$ is the dimension of the cycle space, and a reduction of Lehner and Miraftab, based on a theorem of Richter and Shank, then gives $\mathrm{bn}(G)=O(\log g)$ for graphs of Euler genus $g$ . These orders are best possible.

Posed by Bazargani, Biedl, Bose, Maheshwari and Miraftab, 2024Open 2yModel ChatGPT-5.6 Sol (OpenAI)Solved 2026-09-02

PreprintSignificance 15 Submitted by VibeGene on 3 Sep 2026

Depth-1 distinctness for pseudorandom unitaries

DisprovedAI-discovered

(The paper proves that a tensor-product ensemble of independently chosen single-qubit Clifford gates is (n)-distinct when the number of queries is polynomial in n. This disproves the authors' conjecture that negligibly distinct ensembles must necessarily be entangling. As an application, the depth-log n global Clifford/unitary-2-design layer used in the PFC pseudorandom-unitary construction can be replaced by a single depth-1 layer of local single-qubit 2-designs while preserving the required distinctness property.)

Quantum pseudorandomness

A single layer of independent random single-qubit Clifford gates is $\operatorname{negl}(n)$ -distinct for polynomially many queries. Consequently, in the $PFC$ pseudorandom-unitary construction, the depth- $\log n$ global unitary $2$ -design layer can be replaced by a depth-1 tensor product of single-qubit $2$ -designs while retaining the distinctness property needed for the construction. This provides a counterexample to the conjecture that every negligibly distinct ensemble must be entangling.

Posed by Raza, Eisert and Fefferman (the authors' own working conjecture)Open —Model ChatGPT 5.6 Sol (OpenAI)Solved 2026-09-02

PreprintSignificance 6Submitted by VibeGene on 4 Sep 2026

A Smooth Counterexample to the Trautman Conjecture

DisprovedAI-discovered

(For every neighborhood U of the origin in C×R and every ε>0, Curry constructs a smooth nonnegative perturbation , supported in U with ‖‖_C^2<ε, such that T^0,1_=_ C_\ is strongly pseudoconvex, its canonical bundle admits a nowhere-zero closed section, yet every C^1 CR function near the origin satisfies dh(0)=0. Hence the CR structure is not locally embeddable at the origin. The construction can also be globalized to S^3 as an arbitrarily small C^1 perturbation of the standard spherical CR structure.)

CR geometry

The Trautman conjecture asserted that a smooth three-dimensional CR manifold admitting a nowhere-zero closed section of its canonical bundle must be locally embeddable in $\mathbb{C}^2$ . We modify a standard construction of nonembeddable smooth strongly pseudoconvex CR 3-manifolds so that the condition of having a nowhere-zero closed section of the canonical bundle is preserved, thus providing a strongly pseudoconvex counterexample to the Trautman conjecture.

Posed by Andrzej Trautman, 1998Open 28yModel ChatGPT (model not named; the paper says ChatGPT Plus) (OpenAI)Solved 2026-09-02

PreprintSignificance 25Submitted by VibeGene on 4 Sep 2026

Anari's Bethe permanent conjecture

ProvedAI co-developed

(For every nonnegative n× n matrix A whose bipartite support graph has girth at least an even integer g4, Dong and Jain prove the sharp inequality (A)≤(A)2^2n/g(A). The factor 2^2n/g is optimal whenever g2n, attained by matrices whose support graphs are disjoint unions of g-cycles. Thus the result confirms Anari's conjecture, recovers the sharp 2^n/2 universal Anari--Rezaei bound when g=4, and approaches exactness as the support-graph girth tends to infinity.)

Permanent approximation

For an $n\times n$ nonnegative matrix $A$ , the Bethe permanent, which is computable in deterministic polynomial time, satisfies the tight universal comparison $\operatorname{Bethe}(A) \leq \operatorname{per}(A) \leq 2^{n/2}\operatorname{Bethe}(A).$ The lower bound, due to Gurvits, is attained on forests. The upper bound, due to Anari and Rezaei, is attained by the adjacency matrix of a disjoint union of $4$ -cycles. Confirming a conjecture of Anari, we provide an optimal girth-dependent refinement of the above comparison. More precisely, we show that if the bipartite support graph of $A$ has girth at least an even integer $g \geq 4$ , then $\operatorname{Bethe}(A) \leq \operatorname{per}(A) \leq 2^{2n/g}\operatorname{Bethe}(A).$ The upper bound is attained by the adjacency matrix of a disjoint union of $g$ -cycles.

Posed by Nima AnariOpen —Model ChatGPT 5.6 Sol Ultra (OpenAI)Solved 2026-09-02

PreprintSignificance 22Submitted by VibeGene on 3 Sep 2026

The proper hat-guessing number of $K_5-e$

ProvedUnder reviewAI co-developed

(The exact value is HG_P(K_5-e)=8. The lower bound uses explicit legal twin-player rules over F_2^3. After those rules cover 3,024 of the 8,400 proper colorings, the residual-coloring/local-view incidence graph has left degree three and right degree at most three; Hall's theorem supplies consistent guesses for the three clique players. The release also proves a general sufficient twin-completion lemma for K_n-e. It does not solve the full K_n-e family or determine HG_P(C_5).)

Graph theory; hat-guessing games

Determine the exact proper hat-guessing number of the complete graph on five vertices with one edge removed. The existing bounds left $\mathrm{HG}_P(K_5-e)$ in $\{7,8\}$ .

Posed by Adriaensen et al., 2026Open 0yModel GPT-5.6 Pro (OpenAI)Solved 2026-09-02

AnnouncedSignificance 7 Submitted by Matthew Protti on 2 Sep 2026

A Quantum Oracle Separation Between $\mathsf{QMA}(2)$ and $\mathsf{QMA}$

ProvedAI-discovered

(The authors construct a unitary oracle U such that ^U≠(2)^U. Their black-box problem is solvable by a (2) verifier with one oracle query and linear-size unentangled proofs, whereas any verifier must use either exponentially many queries or an exponentially large witness. As a non-oracle consequence, they prove that for every fixed ε,δ≥ 0 with ε+δ<1, any (ε,δ)-disentangler requires exponentially many input qubits in the number of output qubits, resolving Watrous's no-disentanglers conjecture.)

Quantum complexity theory

We find a quantum oracle relative to which $\mathsf{QMA}\neq\mathsf{QMA}(2)$ . As a consequence, we resolve the no-disentanglers conjecture of Watrous: for every $\varepsilon+\delta<1$ , any $(\varepsilon,\delta)$ -disentangler requires input size exponential in the number of output qubits.

Posed by John Watrous (the no-disentanglers conjecture, as reported by Aaronson, Beigi, Drucker, Fefferman and Shor), 2009Open 17yModel ChatGPT 5.6 Sol (OpenAI)Solved 2026-09-02

PreprintSignificance 36 Submitted by VibeGene on 4 Sep 2026

Common Neighbour Conjectures for Saxl Graphs

DisprovedAI co-developed

(The paper disproves both the Burness–Giudici common neighbour conjecture for primitive groups of base size 2 and its later generalisation to arbitrary base size. For every integer B2, it constructs infinitely many primitive permutation groups of base size B whose generalised Saxl graphs contain two nonadjacent vertices with no common neighbour. At base size 2, it gives infinite counterexample families of affine, product and twisted wreath type, so the conjecture fails in three of the five O'Nan–Scott types.)

Group theory

For a finite permutation group, a base is a set of points with trivial pointwise stabiliser, and the generalised Saxl graph records which pairs of points lie together in a base of minimum size. Burness and Giudici conjectured that any two vertices of the Saxl graph of a primitive group of base size two have a common neighbour, and Freedman, Huang, Lee and Rekvényi extended this conjecture to arbitrary base size. We disprove both. For each integer $B\geq 2$ we construct infinitely many primitive groups of base size $B$ whose generalised Saxl graphs contain two nonadjacent vertices with no common neighbour. At base size two, where this is the usual Saxl graph, we obtain three further infinite families, one each of affine, product and twisted wreath type, so the conjecture fails in three of the five O’Nan–Scott types; in the affine and product type families the Saxl graphs have diameter exactly three. This answers Problem 21.29 in the Kourovka Notebook in the negative. In the positive direction, we prove the Burness–Giudici conjecture for every primitive affine group whose point stabiliser is almost quasisimple of sporadic type, completing work of Lee and Popiel.

Posed by Timothy Burness and Michael Giudici, 2020Open 6yModel ChatGPT Pro; Claude (OpenAI; Anthropic)Solved 2026-09-01

PreprintSignificance 18Submitted by VibeGene on 2 Sep 2026

McKean Entropy-Production Conjecture

DisprovedAI-discovered

(For the space-homogeneous Boltzmann equation in dimension 3 with collision kernels B=1/4π|v-v_*|^γ, γ∈[0,1], the paper constructs smooth, positive, radial mixtures f_R=(1-p)M_1+pM_R for which _tD(f_R)>0 for sufficiently large R. Thus entropy production need not decrease even for Maxwell molecules (γ=0) or hard spheres (γ=1), negatively resolving McKean's monotonicity question for these physically standard kernels.)

Mathematical physics

In 1966, McKean asked whether the entropy production of the Boltzmann equation must be monotone decreasing in time. We show that this is not the case even in the space-homogeneous setting for the Boltzmann collision operator with a constant angular cross section and the kinetic parameter $\gamma\in[0,1]$ . This recovers the classical case of hard spheres and the simplest case of Maxwell molecules. Our examples are radially symmetric mixtures of Maxwellians.

Posed by Henry P. McKean Jr., 1966Open 60yModel GPT-5.6 Sol; Claude (OpenAI; Anthropic)Solved 2026-09-01

PreprintSignificance 20Submitted by VibeGene on 3 Sep 2026

Bounded prime gaps: $H_1 \le 236$

ProvedUnder reviewAI-assisted

(H_1 ≤ 236, between Stadlmann's 240 of 31 August and Axiom Math's 212 of 3 September. Superseded within two days, which Kintali noted himself.)

Analytic number theory

Write $H_1 = \liminf_{n\to\infty}(p_{n+1}-p_n)$ . Announced on 1 September 2026: $H_1 \le 236$ , building on Stadlmann's $240$ of the previous day.

Posed by Alphonse de Polignac (the twin prime conjecture); the bounded form since Goldston, Pintz and Yıldırım, 1849Open 177yModel unspecified AI agentsSolved 2026-09-01

AnnouncedSignificance 62

$(\xi\alpha^n)_{n\ge1}$ is not uniformly distributed modulo one for Pisot $\alpha$ and $\xi$ in the Cantor set $C(\alpha)$

ProvedPartialAI-discovered

(The problem is open, and the repository says so: what is proved are criteria for it and two instances, not the general case. Every compared statement that concludes Problem 10.61 does so for a quadratic setup - a real root α > 1 of X^2 - aX - b whose conjugate has modulus below one - and both instances are quadratic. The arbitrary-degree material is conditional ingredients: for the family X^d - aX^d-1 - 1 the real root exceeding a is shown to be Pisot for a ≥ 3, with a conjugate-modulus bound and a numerical inequality. No compared statement carries those above degree two, because the covering criterion is proved only for quadratic setups. The covering criterion also leaves quadratic α with route-A exponent at least one undecided, about which nothing is claimed.)

Equidistribution mod 1

Bugeaud's Problem 10.61, due to Michel Mendès France in 1967: for a Pisot number $\alpha > 2$ and the Cantor set $C(\alpha) = \{(\alpha-1)\sum_{k\ge1}\varepsilon_k\alpha^{-k} : \varepsilon_k \in \{0,1\}\}$ , no $\xi \in C(\alpha)$ has $(\xi\alpha^n)_{n\ge1}$ uniformly distributed modulo one.

The problem itself remains open. What is proved is a set of criteria for it, and two instances. The criteria: a reduction to symbolic dynamics that is an equivalence; a pressure criterion; and a covering criterion which, for a quadratic setup of norm $b$ , applies exactly when $(\log_2\alpha - 1)(\log_2(\alpha/|b|) - 1) > 1$ , a condition that reduces to $\alpha > 4$ for units. The two instances are both quadratic: at $\alpha = 2+\sqrt5$ in the strong form, an explicit interval that every orbit misses at every time, and at $\alpha = 2+\sqrt3$ by a confinement-gap certificate.

Posed by Michel Mendès France, 1967Open 59yModel Fable 5, Opus 5 (Anthropic)Solved 2026-08-31

Lean-checked, statement unauditedSignificance 22 Submitted by LucidKestrel185 on 31 Aug 2026

A Counterexample to the Stable Forking Conjecture

DisprovedAI co-developed

(The paper constructs a simple theory in which forking cannot always be witnessed by a stable formula. Precisely, what fails is: in a simple theory, if a _C b then there is (x, b) ∈ tp(a/Cb) forking over C whose parameter-free form (x,y) is stable. The counterexample is an infinite-dimensional vector space over the division ring of fractions of the quantum graph algebra of the random graph. Forking is characterised by an abstract independence relation, and the random graph is encoded into that relation so that it has the order property; stable formulas therefore cannot determine all forking in simple theories.)

Model theory

Using ChatGPT 5.6, we find a counterexample to the stable forking conjecture. This answers a long-standing open question of Hart, Kim and Pillay (1996).

Posed by Bradd Hart, Byunghan Kim, and Anand Pillay, 1996Open 30yModel GPT 5.6 Sol (OpenAI)Solved 2026-08-31

PreprintSignificance 26Submitted by VibeGene on 2 Sep 2026

Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication

ProvedPartialAI-assisted

(The exact Mul4 instance is resolved: its unrestricted XOR--AND multiplicative complexity is 9. The restricted bilinear/quadratic value 9 was classical; the new theorem proves that arbitrary nonlinear Boolean reuse cannot lower it. This is a natural positive special case of the Boyar--Find question, not a solution of the general (n,m) problem. The lower bound is a conceptual structural argument. A complete Lean 4 formalization checks the unrestricted circuit semantics and the exact equality, while the development-time Python/C++ programs remain independent regression checks rather than logical premises. The corresponding unrestricted questions for five or more terms remain open. Independent statement-fidelity review remains pending.)

Circuit complexity

Let Mul4: F_2^8 -> F_2^7 output the seven coefficients of the product of two four-term binary polynomials. The manuscript proves that its unrestricted XOR--AND multiplicative complexity is exactly 9. The upper bound is a nine-AND Karatsuba--Ofman construction. The lower bound rules out every unrestricted eight-AND circuit, including circuits that reuse nonlinear intermediate wires and exploit Boolean idempotence. Thus, for this natural vector-valued quadratic function, allowing nonlinear feedback does not improve on the optimal quadratic circuit.

Posed by Joan Boyar and Magnus Gausdal Find, 2014Open 12yModel OpenAI GPT-5.6 Sol (extra-high); Anthropic Opus 5 (high, referee) (OpenAI; Anthropic)Solved 2026-08-31

Site-confirmedSignificance 12 Submitted by SwiftFerret455 on 1 Sep 2026

Local limits along squares and prime values of digital functions

ProvedAI co-developed

(New theorems, not a formalisation of known results. In base ten the bare existence of a square with any admissible digit sum was recorded in the recreational literature (Murthy–Ashbacher 2005); the theorem here is the quantitative all-base version — roots coprime to b (excluding their trailing-zero trick), exp(c_b√q) representations of controlled size — and that statement is what is machine-checked, with effective but non-optimal constants. The same paper proves a local limit theorem for g(n²) for arbitrary digit weights in every base including binary, and sieves the values: level of distribution 1/2, P₃ and P₂ values, an unconditional Mertens-type prime-value law, a joint Erdős–Kac theorem. Caveats: the two shrinking-frequency estimates behind the local theorem enter the Lean development only as transcribed definitions; the sieve and asymptotic results are unformalised; Corollary 1.9 is formalised in bases 2 and 3 only; the analogous theory along squares of primes remains open.)

Digital problems; local limit theorems; Sidon sets; sieve methods

Call an integer admissible if it is congruent to a square modulo b−1 (for b = 2 the condition is vacuous). For every base b ≥ 2 there are constants c_b, C_b > 0 such that the following holds: if q is sufficiently large and admissible, then

#{n ≥ 1 : (n,b) = 1, s_b(n²) = q, n² ≤ b^{C_b·q}} ≥ exp(c_b·√q).

The Lean 4 formalisation proves the explicit form: at least 2^{√q/(36b)} representations of size n² ≤ b^{3q} once q ≥ 2304·b⁴.

Posed by Murthy–Ashbacher (base ten, recreational), 2005Open 21yModel Claude Opus 5, Claude Fable 5, OpenAI Sol (Anthropic, OpenAI)Solved 2026-08

Lean-checked, statement unauditedSignificance 12 Submitted by vibefrtz on 29 Aug 2026

Prime values of digital functions along the primes

ProvedAI co-developed

(For every integer-valued strongly b-additive g with (g(1),…,g(b-1))=1 and digit mean _g0: g(p) is prime for infinitely many primes p. For _g>0, ∑ 1/p over p<X with g(p) prime is (d_g/(d_g))log_3X + C_g,1 + O(1/loglog X), likewise for the first j iterates. Also \#≤ x: g(p) prime\≪π(x)/loglog x, of that exact order on a large set of x, and (g(p)) has normal order log_3 p. What is new and what is not. For the digit sum g=s_b, Harman (2012) already proved both the infinitude and a Mertens formula; the new information there is the remainder tending to a limit rather than being O(1), and the iterated version for g=s is, in the paper's words, "contained, in a stronger and quantitative form, in Harman". The new content is the generalization to every such g, which delivers the running example g=S, the sum of squared decimal digits, and so the infinitude of OEIS A052034.)

Analytic number theory

Every integer-valued strongly b-additive function g with gcd(g(1),…,g(b−1)) = 1 and nonnegative digit mean takes prime values at infinitely many primes, with a Mertens-type formula and normal-order results; the running example resolves the infinitude of OEIS A052034 (De Geest, 1999): infinitely many primes have a prime sum of squared decimal digits.

Posed by —, 1999Open 27yModel Claude Opus 5, Claude Fable 5 (Anthropic)Solved 2026-08

Lean-checked, statement unauditedSignificance 11 Submitted by vibefrtz on 26 Aug 2026

An Erdős–Kac law for base- $b$ palindromes and for reversed primes

ProvedAI co-developed

(New theorems, not a formalisation of previously known results. For every base b2 the Erdős–Kac law is established for the λ-digit base-b palindromes and for the base-b reversals of the λ-digit primes, for and Ω and for _S,Ω_S with any regular set S of primes; with normal order loglog n on both families, and, for , all moments of order up to 12(loglog b^λ)^1/3 uniformly in the order. For reversed primes it also holds with the leading digit prescribed. Not settled: the results rest on quoted inputs (Col for palindromes, the Bombieri–Vinogradov theorem of Dartyge–Rivat–Swaenepoel for reversed primes), and both families exclude the primes dividing b(b^2-1). No rate of convergence is obtained. The question of Banks–Shparlinski on the *largest* value of on palindromes is untouched: the trivial bound ≪λ/logλ and their λ^o(1) remain far apart.)

Analytic number theory

For every base $b\ge2$ , the number of prime factors of the $\lambda$ -digit base- $b$ palindromes, and of the base- $b$ reversals of the $\lambda$ -digit primes, obeys an Erdős–Kac law: counted with or without multiplicity, it is asymptotically normal with centring $\log\log b^{\lambda}$ and scaling $\sqrt{\log\log b^{\lambda}}$ . For reversed primes the law persists when the leading digit of the prime is prescribed. Erdős–Kac laws were already known for other digitally defined families — integers with a fixed digit sum, or with digits restricted to a fixed set — but for palindromes only the largest value of $\omega$ had been studied, with nothing known about the typical value, and for reversed primes the level of distribution the argument needs became available only in 2025.

Posed by —Open —Model Claude Fable 5, Claude Opus 5 (Anthropic)Solved 2026-08

Lean-checked, statement unauditedSignificance 12 Submitted by vibefrtz on 24 Aug 2026

…

$(\xi\alpha^n)_{n\ge1}$ is not uniformly distributed modulo one for Pisot $\alpha$ and $\xi$ in the Cantor set $C(\alpha)$

ProvedPartialAI-discovered

Equidistribution mod 1

Posed by Michel Mendès France, 1967Open 59yModel Fable 5, Opus 5 (Anthropic)Solved 2026-08-31

Lean-checked, statement unauditedSignificance 22 Submitted by LucidKestrel185 on 31 Aug 2026

Math problems solved with AI

Latest activity

Latest

This week

All entries