VibeMathed - Math Problems Solved by AI

9 min read Original article ↗

Tracked problems
295
207 fully resolved

Combined years open
5,192
before AI closed them

Lean-verified
126
machine-checked

Community members
68
57 votes · 14 comments

Latest activity

Edits, submissions and discussion

All entries

ProvedUnder reviewAI-assisted

(The Formal Conjectures pull request flipping this from open to solved is still open rather than merged, so the canonical repository has not yet accepted it.)

Graph Theory (automated conjecture)

For every finite connected simple graph GG, is the order of the largest induced tree at least girth(G)1+ecc(G,center(G))\mathrm{girth}(G) - 1 + \mathrm{ecc}(G, \mathrm{center}(G)), where the last term is the eccentricity of the centre set? Answered affirmatively, with a Lean proof.

Posed by Written on the Wall II (automated conjecturing)Open Model ChatGPT + Codex (OpenAI)Solved 2026-08-03

Lean-verifiedSignificance 5

ProvedUnder reviewAI-discovered

(The formalization proves the statement under the weaker hypothesis n >= 2; the pull request marking the conjecture solved is open, not merged)

Graph theory (automated conjecture)

Let GG be a simple connected graph on n5n\geq 5 vertices. If the maximum over all vertices vv of (v)\ell(v) - the independence number of the subgraph induced by the open neighborhood N(v)N(v) - is at most 11, must GG be well totally dominated? Answered affirmatively; the Lean proof in fact needs only n2n\geq 2, and retains the conjecture's n5n\geq 5 to state the source faithfully.

Posed by Written on the Wall II (automated conjecturing)Open Model Aristotle (Harmonic)Solved 2026-08-02

Lean-verifiedSignificance 5

DisprovedUnder reviewAI-discovered

Erdős #146 · Extremal graph theory

If HH is bipartite and rr-degenerate, is ex(n;H)n21/r\mathrm{ex}(n;H) \ll n^{2-1/r} (a \$500 Erdős-Simonovits prize conjecture)? A counterexample refutes the degeneracy conjecture.

Posed by Paul Erdős, Miklós Simonovits, 1984Open 42yModel Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 25

DisprovedUnder reviewAI-discovered

Geometric group theory

Is every group sofic - does every group admit approximate finite permutation representations? A central open question of geometric group theory since Gromov introduced soficity: soficity implies Gottschalk's surjunctivity conjecture, Kaplansky's stable finiteness and more, and no non-sofic group was known. An explicit construction now establishes that non-sofic groups exist.

Posed by Mikhail Gromov, Benjamin Weiss, 1999Open 27yModel Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 60

1comment

ProvedUnder reviewAI-discovered

Convex geometry

What is the maximum volume of a convex body in Rn\mathbb{R}^n whose centroid is its only interior lattice point? Ehrhart conjectured the extremal value in 1964; the sharp maximum is now determined in every dimension.

Posed by Eugène Ehrhart, 1964Open 62yModel Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 25

2comments

DisprovedUnder reviewAI-discovered

Operator algebras

Are ICC property (T) groups remembered by their von Neumann algebras - if L(Γ)L(Λ)L(\Gamma) \cong L(\Lambda) for such groups, must ΓΛ\Gamma \cong \Lambda? A counterexample refutes Connes' conjecture that these groups are uniquely determined by their group von Neumann algebras.

Posed by Alain Connes, 1980Open 46yModel Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 45

DisprovedUnder reviewAI-discovered

Erdős #180 · Extremal graph theory

For every finite family F\mathcal{F} of graphs, is there a single GFG \in \mathcal{F} with ex(n;G)Fex(n;F)\mathrm{ex}(n;G) \ll_{\mathcal{F}} \mathrm{ex}(n;\mathcal{F})? A counterexample refutes the Erdős-Simonovits compactness conjecture.

Posed by Paul Erdős, Miklós Simonovits, 1982Open 44yModel Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 20

ProvedUnder reviewAI co-developed

(Claimed in a self-published research draft; a standalone by-product is the transcendence of the integral of exp(q) between distinct algebraic endpoints for nonconstant algebraic q)

Commutative Algebra, Transcendence

Let L(xayb)=a!b!\mathcal{L}(x^{a}y^{b})=a!\,b! on C[x,y]\mathbb{C}[x,y]. The Factorial Conjecture asks whether L(fm)=0\mathcal{L}(f^{m})=0 for every m1m\geq 1 forces f=0f=0. The homogeneous two-variable case was settled by Liu and Sun; the inhomogeneous problem does not reduce to it, because radial integration couples the homogeneous layers through Gamma factors. A claimed proof settles the full two-variable case affirmatively.

Posed by Arno van den Essen, David Wright, Wenhua Zhao, 2011Open 15yModel GPT-5.6 Sol, Claude Opus 5 (OpenAI, Anthropic)Solved 2026-08-01

AnnouncedSignificance 20

ProvedUnder reviewAI-discovered

Lattices & cryptography

Is the closest vector problem NP-hard to approximate within polynomial factors ncn^c? Yes for some c>0c > 0: hardness of approximation reaches polynomial factors, with consequences for decoding and related lattice problems - a foundational question underpinning post-quantum cryptography where hardness had stalled at almost-polynomial factors since the late 1990s.

Posed by Open Model Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 35

ProvedUnder reviewAI-discovered

Erdős #183 · Ramsey theory

Let R(3;k)R(3;k) be the least nn such that every kk-colouring of the edges of KnK_n contains a monochromatic triangle. Determine limkR(3;k)1/k\lim_{k\to\infty} R(3;k)^{1/k} (a \$250 Erdős prize problem). A superexponential lower bound resolves the problem: the limit is infinite.

Posed by Paul Erdős, 1961Open 65yModel Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 20

ProvedPartialAI-discovered

(upper bounds reach the Cohn-Elkies threshold; the true asymptotic density remains open)

Discrete geometry

How dense can a sphere packing in Rn\mathbb{R}^n be as nn \to \infty? The Kabatiansky-Levenshtein upper bound stood for almost fifty years; the new proof improves the asymptotic upper bound all the way down to the Cohn-Elkies linear-programming threshold.

Posed by , 1978Open 48yModel Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 50

ProvedPartialAI-discovered

(exponential improvement over the 1977 MRRW bounds; the exact rate-distance trade-off remains open)

Coding theory

What is the maximum size of a binary code of given minimum distance? The linear-programming bounds of McEliece, Rodemich, Rumsey and Welch (1977) resisted improvement for half a century. The new upper bounds are exponentially stronger at every prescribed distance, with analogous results for high-dimensional spherical codes.

Posed by , 1977Open 49yModel Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 40

ProvedUnder reviewAI-discovered

Quantum complexity

Does the value of a two-player quantum game decay exponentially under parallel repetition, as Raz's theorem gives for classical games? Yes: an exponential parallel repetition theorem holds for arbitrary finite two-player quantum games.

Posed by Open Model Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 25

ProvedPartialAI-discovered

(an n^4/log n formula lower bound; VP vs VNP remains wide open)

Algebraic complexity

How large must arithmetic circuits and formulas computing the n×nn \times n permanent be? New lower bounds include an arithmetic-formula bound of order n4/lognn^4/\log n, far beyond the quadratic barrier that stood for decades.

Posed by Leslie Valiant, 1979Open 47yModel Astra (internal preview) (OpenAI)Solved 2026-08-01

Lean-verifiedSignificance 40

ProvedAI-assisted

(The ball case. For arbitrary domains Pólya's conjecture remains open; this continues the authors' programme after the planar disk, circular sectors, and the Dirichlet case in arbitrary dimensions.)

Spectral Geometry, Laplace Eigenvalues

Pólya conjectured in 1954 that the Weyl-law expression bounds the eigenvalue counting function of the Laplacian. The paper proves the Neumann case for Euclidean balls in dimensions three and higher, extending the authors' earlier planar and Dirichlet results. Key difficulty: estimating zeros of derivatives of ultraspherical Bessel functions rather than of Bessel functions themselves.

Posed by George Pólya, 1954Open 72yModel ChatGPT + Claude (several models)Solved 2026-07-31

PreprintSignificance 35

ProvedPartialAI co-developed

(Record lower bound only. The sub-2 ceiling is the codimension-two case and does not bound the record ladder (k=17 has complement mass 11). 4/3 and 2 are conjectures; the proved gap is [1.28249, 2].)

For a single-source unsplittable flow, find the optimal universal additive constant CC s.t. every feasible fractional flow xx with arc costs cc should admit an unsplittable routing yy with cycxc^\top y \le c^\top x and yaxa+Cdmaxy_a \le x_a + C \cdot d_{\max} on every arc. Goemans conjectured C=1C=1; this was disproved in July 2026 by a separate seven-vertex counterexample with critical constant 16/1516/15 (see the Dinitz–Garg–Goemans entry), leaving the optimal CC open. Lower bound: a seventeen-terminal common-point interval instance certifies C  12824947979848435211018=1.28249 C\ \ge\ \frac{1282494797984843521}{10^{18}}=1.28249\ldots Upper bounds: the paper proves the first unconditional ceiling below 2, but for the codimension-two case only, at complement mass q=2q=2. The record cells lie outside it — the k=17k=17 instance has q=11q=11 — so that ceiling does not bound the record ladder. Two figures are conjectures rather than results: 4/34/3 as the supremum of critical constants over common-point cells, approached but not attained and not an extrapolation from the ladder (Conjecture 1.1, Theorem 5.1), and 22 for the universal constant itself (Conjecture 1.2). The proved gap remains [1.28249, 2][1.28249\ldots,\ 2].

Posed by Dinitz, Garg, Goemans, 1999Open 27yModel GPT-5.6 Sol, Claude Fable 5, Claude Opus 5 (OpenAI, Anthropic)Solved 2026-07-31

Site-confirmedSignificance 15Submitted by BraveDingo215

5comments

ProvedUnder reviewAI-discovered

Graph theory (automated conjecture)

Posed by Written on the Wall II (automated conjecturing)Open Model Claude Opus 5 (with Gemini 3.1 Pro, GPT-5.3 Codex Spark, Grok 4.5)Solved 2026-07-30

Lean-verifiedSignificance 5

ProvedPartialAI-discovered

(four record lower bounds; the exact capacities remain open for every odd cycle beyond C5)

Zero-error information theory

Determine the Shannon capacities of odd cycles beyond C5C_5, or improve the best explicit bounds. New independent sets in strong graph powers give Θ(C7)>3.258020\Theta(C_7) > 3.258020, Θ(C11)>5.289773\Theta(C_{11}) > 5.289773, Θ(C13)>6.300109\Theta(C_{13}) > 6.300109 and Θ(C15)>7.301399\Theta(C_{15}) > 7.301399.

Posed by Claude Shannon, 1956Open 70yModel ChatGPT-5.6 Sol Pro (OpenAI)Solved 2026-07-30

PreprintSignificance 35

ProvedAI co-developed

(leading asymptotic determined up to a bounded q-dependent term)

Function-field arithmetic

Let Dq(n)D_q(n) be the largest possible least degree of a polynomial omitted by a non-covering family of nn distinct-modulus congruence classes in Fq[x]\mathbb{F}_q[x]. What is its asymptotic size? The answer is Dq(n)=nq1+Oq(1)D_q(n) = \frac{n}{q-1} + O_q(1).

Posed by Open Model ChatGPT-5.6 Sol (OpenAI)Solved 2026-07-30

PreprintSignificance 10

2comments

DisprovedUnder reviewAI-discovered

(Infinite family of counterexamples; mathematical argument internally checked, with external verification and novelty review pending.)

Graph theory

Every finite connected simple graph G satisfies α(G)r(G)+ln(ρ(G)),\alpha(G)\ge r(G)+\ln(\rho(G)), where α(G)\alpha(G) is the independence number, r(G)r(G) is the radius, and ρ(G)\rho(G) is the minimum number of pairwise vertex-disjoint paths whose vertices cover V(G)V(G).

Posed by Graffiti, reported by Ermelinda DeLaViña, Siemion Fajtlowicz, and Bill Waller, 2002Open 24yModel GPT-5.6 Thinking (OpenAI)Solved 2026-07-30

AnnouncedSignificance 5Submitted by Lamp

DisprovedAI-discovered

(no constant-bound repair of the conjecture is possible)

Spectral graph theory

Is the difference between the numbers of positive and negative adjacency eigenvalues of every connected line graph at most one? A 1414-vertex witness has signature 22, and chaining copies gives connected line graphs of signature k+1k + 1 for every k1k \ge 1 - the signature is unbounded.

Posed by Saieed Akbari et al., 2026Open 0yModel ChatGPT-5.6 Pro, Claude Fable 5 (OpenAI / Anthropic)Solved 2026-07-30

PreprintSignificance 5

ProvedAI co-developed

Commutative Algebra, Local Cohomology

Can a noetherian ring have a local cohomology module whose support is not closed - equivalently, one with infinitely many minimal primes? Huneke and Lyubeznik asked; the paper constructs such rings, so the answer is yes.

Posed by Craig Huneke and Gennady LyubeznikOpen Model ChatGPT 5.5 / 5.6 (OpenAI)Solved 2026-07-30

PreprintSignificance 25

DisprovedUnder reviewAI-discovered

Spectral graph theory

Does every nontrivial finite simple graph have noninteger Sombor energy? If ρ1,,ρn\rho_1,\ldots,\rho_n are the eigenvalues of the Sombor matrix of a graph GG, its Sombor energy is ESO(G)=i=1nρi.E_{\mathrm{SO}}(G)=\sum_{i=1}^{n}|\rho_i|. The conjecture asserted that ESO(G)ZE_{\mathrm{SO}}(G)\notin\mathbb Z for every nontrivial graph. A connected graph on nine vertices is exhibited with ESO(G)=64E_{\mathrm{SO}}(G)=64, disproving the conjecture.

Posed by Nima Ghanbari, 2021Open 5yModel GPT-5.6 Thinking (OpenAI)Solved 2026-07-30

AnnouncedSignificance 5Submitted by Lamp

DisprovedAI co-developed

Classical electrostatics

Do nn point charges whose electrostatic potential has only non-degenerate critical points always have at most (n1)2(n-1)^2 of them? A configuration of five charges - three at the vertices of an equilateral triangle plus two small central charges pulled apart into a shallow bipyramid - has at least 24>1624 > 16 non-degenerate critical points, so the conjecture is false.

Posed by James Clerk Maxwell, 2004Open 22yModel GPT-5.6 Sol (OpenAI)Solved 2026-07-29

PreprintSignificance 30

ProvedAI-discovered

(New arXiv preprint with an author-provided Lean formalization; not yet peer-reviewed.)

Additive combinatorics

For every finite set AZA\subset\mathbb Z with A2|A|\ge 2, define C(A)=log(A+A/A)log(AA/A).C(A)=\frac{\log\left(|A+A|/|A|\right)} {\log\left(|A-A|/|A|\right)}. Determine the largest possible value of C(A)C(A), equivalently the least universal exponent cc such that A+AA(AAA)c\frac{|A+A|}{|A|} \le \left(\frac{|A-A|}{|A|}\right)^c for every such set AA. The result proves that the supremum is exactly 22, although no individual admissible set attains it.

Posed by Open Model Hy3 (Tencent Hunyuan)Solved 2026-07-29

Lean-verifiedSignificance 20Submitted by matthew

2comments