Open Math Problems Claimed to Be Solved with AI

SearchLean checked only

Model / system

How verification is classified

Lean checked means the encoded proposition was accepted by Lean’s kernel in the cited environment.

Statement fidelity is separate: the Lean proposition must still be compared with the intended informal problem.

End to end excludes decisive results left as assumptions, axioms, or sorry.

Claim issues collects withdrawn novelty claims, statement mismatches, and incomplete formalizations.

Algebra

21 May 2026Commutative algebra

Log-concavity of codimension-three pure O-sequences

Problem statement

For a pure O-sequence

h=(h_0,\ldots,h_e)

of codimension three and type two, is

h_i^2\geq h_{i-1}h_{i+1}

for every interior index

i

Every pure O-sequence of codimension three and type two is proved log-concave. The broader nonmonomial level-Hilbert-function case remains open.

Details and sources

AI contribution

The system reformulated the combinatorial structure and supplied a substantial case analysis, then translated the argument into Lean.

Verification

Lean checked

Publication

AP Nexus preprint and public formal development

Activity evidence

A recent explicit conjecture inside a sustained specialist program on Hilbert functions and pure O-sequences.

The monomial pure-O-sequence statement is complete, but it must not be conflated with the wider level-algebra conjecture.

AP Nexus paper Original conjecture paper Formal development

Precise monomial case proved

System: AlphaProof Nexus
Verification: Lean checked
Open for: 4 years
Research activity: 3/5

10 Jun 2026Algebraic combinatorics

Hook coefficients of universal Hilbert series

Problem statement

For the universal Schur coefficients

c_\lambda(n)

in the multigraded Hilbert series of the coinvariant algebra

R_n^{(m)}

, give a combinatorial interpretation when

\lambda

is a hook partition.

ProofCouncil, UCLA Moonshot, and ChatGPT 5.5 Pro each produced a correct combinatorial interpretation. The editors requested only minor revisions, mostly for exposition and citation placement.

Details and sources

AI contribution

Three systems independently derived hook-shape formulas using ordered set partitions or related combinatorial encodings; the reviewers noted that several differed from the human solution.

Verification

Double-blind expert review; minor revisions

Publication

First Proof Second Batch report, complete submissions, logs, and referee reports

Activity evidence

The problem combines active work on diagonal coinvariants, superspace, Schur expansions, and sign-reversing involutions.

The result belongs to a forthcoming project on universal Hilbert-series coefficients of superspace coinvariant rings. The public report supplies both the intended result and detailed referee judgments.

First Proof benchmark and source files Official report and referee decisions Problems, submissions, reviews, and logs

Research problem solved

System: GPT-5.5 Pro / ProofCouncil / UCLA Moonshot
Verification: Double-blind expert review; minor revisions
Open for: Unpublished algebraic-combinatorics problem
Research activity: 3/5

12 Jun 2026Finite group theory

Solubilizer Conjecture A.1

Problem statement

G

is nonsolvable and

\operatorname{Sol}_G(x)\cap\operatorname{Sol}_G(y)

is nonempty, must that intersection contain a nontrivial normal subgroup of

G

The alternating group $A_5$ and a five-cycle give a counterexample: the relevant solubilizer is $D_{10}$ and contains no nontrivial normal subgroup of $A_5$ .

Details and sources

AI contribution

The system generated an explicit group-theoretic certificate, independent recomputations, a clean-room checker, and mutation tests.

Verification

Dual computational routes; not externally refereed

Publication

Public certificate, checker, source snapshot, and write-up

Activity evidence

A recent appendix conjecture produced in an AI-math workshop project; the mathematical weight is modest and the wording matters.

This refutes the printed phrase “normal subgroup of $G$ .” A charitable alternative meaning “normal in the intersection” is not refuted.

Original conjecture collection Certificate and checker Verification catalog and runnable checks Verification method and limitations

Conjecture refuted as printed

System: Demonstrandum multi-agent pipeline
Verification: Dual computational routes; not externally refereed
Open for: LLM-generated workshop-paper conjecture
Research activity: 1/5

12 Jun 2026Finite group theory

Solubilizer Conjecture A.13

Problem statement

\operatorname{Sol}_G(x)

is a proper subgroup of a nonsolvable finite group

G

, must the intersection of all its conjugates lie in the hypercenter of

G

For $G=A_5\times S_3$ and a five-cycle in the first factor, the solubilizer’s normal core contains $1\times S_3$ while the hypercenter of $G$ is trivial.

Details and sources

AI contribution

The pipeline produced a finite certificate, a mutation-tested checker, and an independent clean-room recomputation.

Verification

Audit-panel grade; one banked checker; not externally refereed

Publication

Public certificate, checker, source snapshot, and audit log

Activity evidence

A recent AI-generated conjecture that the original authors reported they could not computationally validate.

The two plausible quantifier readings of “its conjugates” are checked to be equivalent here. Novelty evidence is literature-search based.

Original conjecture collection Certificate, checker, and audit Verification catalog and runnable checks Verification method and limitations

Conjecture refuted as printed

System: Demonstrandum multi-agent pipeline
Verification: Audit-panel grade; one banked checker; not externally refereed
Open for: Previously unvalidated workshop-paper conjecture
Research activity: 1/5

12 Jun 2026Finite group theory

Solubilizer Conjecture A.16

Problem statement

\operatorname{Sol}_G(x)

is a proper subgroup of a nonsolvable finite group

G

, must its intersection with its normalizer be metabelian?

For $G=A_5\times S_4$ , the relevant proper self-normalizing solubilizer is $D_{10}\times S_4$ , whose derived length is three rather than metabelian.

Details and sources

AI contribution

The system supplied a brute-force finite-group certificate, a mutation-tested checker, and an independent recomputation.

Verification

Audit-panel grade; one banked checker; not externally refereed

Publication

Public certificate, checker, source snapshot, and audit log

Activity evidence

A recent AI-generated appendix conjecture with a direct finite counterexample.

The concrete group is completely checked. The accompanying product template is explanatory and does not turn every related solubilizer conjecture into a theorem.

Original conjecture collection Certificate, checker, and audit Verification catalog and runnable checks Verification method and limitations

Conjecture refuted as printed

System: Demonstrandum multi-agent pipeline
Verification: Audit-panel grade; one banked checker; not externally refereed
Open for: Previously unvalidated workshop-paper conjecture
Research activity: 1/5

4 Apr 2026Commutative algebra

Anderson’s quasi-completeness question

A weakly quasi-complete Noetherian local ring that is not quasi-complete gives a counterexample to D. D. Anderson’s 2014 question.

Details and sources

AI contribution

Rethlas found the construction using mathematical retrieval; Archon translated it into Lean and filled nontrivial gaps.

Verification

Lean checked + statement comparator

Publication

Public preprint, complete Lean project, and open-source agents

This is an unusually complete audit trail: the informal proof, formal statement, kernel-checked development, references, and raw model output are all available.

Preprint Lean formalization Rethlas source Archon source

Question answered negatively

System: Rethlas + Archon
Verification: Lean checked + statement comparator

3 Feb 2026Numerical semigroups

Fel’s conjecture on syzygies

The conjectured universal formula for normalized alternating syzygy power sums of numerical semigroup rings was proved for every index.

Details and sources

AI contribution

Starting from a natural-language specification, AxiomProver generated the mathematical proof and a Lean/Mathlib development.

Verification

Lean checked + multi-author audit

Publication

Public arXiv preprint with a complete formal proof

The theorem was open as a mathematical conjecture, rather than merely an already-known result newly encoded in Lean.

Preprint

Conjecture proved and formalized

System: AxiomProver
Verification: Lean checked + multi-author audit

Analysis

6 May 2026Functional analysis and inequalities

Carbery’s almost-orthogonality inequality in $L^p$

Problem statement

For p ≥ 2, does Carbery’s proposed many-function almost-orthogonality inequality hold with the pairwise overlap coefficients raised to the power 2? If not, what is the largest possible exponent?

The proposed exponent 2 fails for every p > 2. The paper identifies the necessary critical exponent p′ and proves the corresponding inequality for every integer p ≥ 2, together with an optimal three-function bound.

Details and sources

AI contribution

Grok supplied the structural counterexample and a central kernel inequality. The later theorems were developed through a documented human–AI collaboration, with the authors correcting numerical inaccuracies in the first model output.

Verification

Author-checked public proof

Publication

Complete arXiv paper with conventional proofs and disclosed Grok conversations

Activity evidence

A 2009 question connected to sustained work on sharpened triangle inequalities, Schatten classes, and optimal moment comparisons.

The authors state that they already expected a counterexample, but Grok found the conceptual construction that exposed the sharp exponent. The published argument is the authors’ checked and edited version.

Research paper Readable full paper and chat appendix

Question disproved; sharp form proved

System: Grok Heavy / Grok 4.20 Heavy
Verification: Author-checked public proof
Open for: 17 years
Research activity: 4/5

12 Feb 2026Scattering amplitudes

Single-minus gluon tree amplitudes

Problem statement

Do the tree-level amplitudes

A_n(1^-,2^+,\ldots,n^+)

vanish identically, or can they be nonzero in half-collinear kinematics—and if nonzero, what is their all-

n

closed form?

Single-minus tree amplitudes, often presumed to vanish, are shown to be nonzero on half-collinear complex kinematics, with a piecewise-constant closed formula for every multiplicity.

Details and sources

AI contribution

GPT-5.2 Pro conjectured the all- $n$ formula from human-computed low-point cases; a scaffolded internal model produced a proof later checked analytically by the authors.

Verification

Analytically checked by authors

Publication

Public preprint submitted for publication

Activity evidence

Scattering amplitudes are a large international research program, and the degenerate single-minus configuration had been a recurring specialist question for roughly fifteen years.

This is a new theorem in mathematical physics rather than the settlement of a named conjecture, so it is classified as a variant result.

Research paper OpenAI research account

Long-standing presumption overturned

System: GPT-5.2 Pro
Verification: Analytically checked by authors
Open for: Question pursued for about 15 years
Research activity: 4/5

Feb 2026Potential theory and polynomials

Erdős Problem #1040 — polynomial sublevel-set measure

Problem statement

For a closed infinite set

F\subseteq\mathbb C

, let

\mu(F)

be the infimum of

|\{z:|f(z)|<1\}|

over monic polynomials whose zeros lie in

F

. Is

\mu(F)

determined only by the transfinite diameter of

F

Aletheia produced closed sets of equal transfinite diameter but sharply different values of the polynomial sublevel-set invariant, disproving the claim that capacity alone determines it. The zero-measure clause remains separate.

Details and sources

AI contribution

The agent autonomously searched for contrasting sets, tested the construction, and wrote the released argument.

Verification

Expert-reviewed project result

Publication

DeepMind paper, released output, and official problem discussion

Activity evidence

A long-standing specialist problem linked to classical logarithmic potential theory and extremal polynomial questions.

The compound Erdős entry contains more than one question. This result settles only the capacity-determination clause.

Official problem record Erdős case-study paper Aletheia system paper Released Aletheia outputs

First question answered negatively

System: Aletheia / Gemini Deep Think
Verification: Expert-reviewed project result
Open for: 68 years
Research activity: 3/5

9 Jun 2026Global inversion and neural networks

Neural Jacobian Conjecture at width $N=n+1$

Problem statement

If a one-hidden-layer affine-ridge sigmoid network

F:\mathbb R^n\to\mathbb R^n

has strictly positive Jacobian determinant everywhere, must it be globally injective? The proved case has width

N=n+1

Two models independently proved the newly proposed conjecture for one-hidden-layer affine-ridge sigmoid networks at width $N=n+1$ . The cases $N\geq n+2$ remain open.

Details and sources

AI contribution

Moonshine generated the conjecture and invoked the two models independently; an additional ChatGPT web-session collaboration produced a geometric-topological proof.

Verification

Multiple proofs in public preprint

Publication

Public Moonshine arXiv paper

Activity evidence

A new conjecture introduced in the same paper as its first special-case proofs, with little independent follow-up yet.

Because the conjecture and proof appeared together in 2026, the activity and age fields deliberately remain low.

Moonshine paper

First nontrivial width proved

System: GPT-5.5 Pro / DeepSeek-V4 Pro
Verification: Multiple proofs in public preprint
Open for: Newly posed in 2026
Research activity: 1/5

16 Mar 2026Kinetic partial differential equations

Equilibria of the Vlasov–Maxwell–Landau system

Problem statement

Under the paper’s smoothness, positivity, Schwartz-decay, and score assumptions, are all steady solutions of the Coulomb Vlasov–Maxwell–Landau system necessarily spatially uniform Maxwellians?

Every smooth positive Coulomb Vlasov–Maxwell–Landau steady state on $\mathbb T^3\times\mathbb R^3$ satisfying the stated decay and score bounds is a spatially uniform Maxwellian, with zero electric field and constant magnetic field.

Details and sources

AI contribution

Gemini supplied the proof blueprint, Claude Code built more than ten thousand lines of Lean, and Aristotle closed the remaining lemmas; humans audited the definitions.

Verification

Lean checked end to end

Publication

Public preprint, Lean repository, and complete interaction logs

Activity evidence

The exact characterization is new, although it lies inside the large and active kinetic-PDE and plasma-physics literature.

The theorem has explicit regularity, positivity, velocity-decay, and score assumptions. The paper also records human corrections to definition alignment during formalization.

Research paper Lean development Public interaction logs

Conjecture proved under explicit hypotheses

System: Gemini Deep Think / Claude Code / Aristotle
Verification: Lean checked end to end
Open for: Precise conjecture posed in 2026
Research activity: 2/5

17 May 2026Complex analysis

Erdős Problem #1039 — inradius of polynomial lemniscates

Problem statement

For

f(z)=\prod_{i=1}^n(z-z_i)

with

|z_i|\leq1

, let

\rho(f)

be the radius of the largest disc contained in

\{z:|f(z)|<1\}

. Is

\rho(f)\gg1/n

, and what is its exact extremal behavior?

The largest-disc radius is proved to have worst-case order $\Theta(1/n)$ , including the explicit lower bound $\rho(f)\geq(\log2)/n$ . The exact asymptotic constant remains unknown.

Details and sources

AI contribution

GPT-5.5 Pro supplied the proof; Codex assisted the subsequent Lean formalization.

Verification

Expert-vouched and Lean checked

Publication

Public output, official discussion, and Lean repository

Activity evidence

A 1958 complex-analysis problem with Pommerenke’s classical bound, a 2025 paper, and extensive current expert discussion.

This fully answers the order-of-magnitude subquestion but not the complete request to determine the extremal radius.

Official problem record Research discussion Lean repository

Order of magnitude determined

System: GPT-5.5 Pro / Codex 5.5
Verification: Expert-vouched and Lean checked
Open for: 68 years
Research activity: 4/5

3 Mar 2026Complex analysis

Derivative bounds for polynomial lemniscates

Problem statement

For a degree-

n

polynomial with connected unit lemniscate, is the maximum of

|p'|

at most

(1/2+o(1))n^2

The Eremenko–Lempert theorem was formalized in Lean with an open-source proof scaffold and proprietary model backends.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle / Claude Opus 4.6 / Claude Sonnet 4.6 / Gemini 3 Flash / Gemini 3.1 Pro / ulam.ai scaffold with Gemini 3 Flash and Gemini 3.1 Pro
Verification: Lean checked

30 Dec 2025Complex analysis

Projection lengths of polynomial lemniscates

Problem statement

Must every monic non-constant polynomial have a straight line onto which its unit lemniscate projects with length at most two?

Aristotle produced and checked the explicit counterexample $p(z)=z^{16}-1$ ; GPT located related prior literature.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle / GPT
Verification: Lean checked

21 Jan 2026Complex analysis

Convexity of small lemniscate components

Problem statement

Let

f\in\mathbb C[x]

be monic with

m

distinct roots, and let

c>0

be small enough that

\{z:|f(z)|\leq c\}

has

m

connected components. Must all those components be convex?

Aristotle generated a formal counterexample and verified it in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

28 Jan 2026Complex analysis

Diameter of a lemniscate component

Problem statement

If every root of a monic polynomial lies in

|z|\leq r<2

, must some component of its unit lemniscate have diameter greater than

2-r

The bound is false for $r>1$ but true for $0<r\leq1$ ; the counterexample and positive range were formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

29 Dec 2025Complex analysis

Entire functions preserving rationality

Problem statement

Does a nonlinear entire function exist such that

x

is rational exactly when

f(x)

is rational?

The classical affirmative construction was reconstructed and checked in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

28 Dec 2025Entire functions

Prescribed derivative-zero sets

Problem statement

Given discrete sets

S_n\subset\mathbb C

, can one transcendental entire function have some derivative vanish on every point of each

S_n

The Barth–Schneider affirmative theorem was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

2 Jun 2026Mathematical statistical physics

FullRSB jamming identity $a+b=1$

Problem statement

Can the numerically observed fullRSB critical-exponent relation

a+b=1

at the jamming transition be derived analytically from the scaling equations?

Parisi and Zamponi proved analytically that the full replica-symmetry-breaking jamming exponents satisfy $a+b=1$ , an identity previously observed only numerically to high precision.

Details and sources

AI contribution

The authors state that the proof was obtained through interaction with Claude Sonnet 4.6 and Opus 4.7 and then verified by them.

Verification

Author verified and journal published

Publication

Journal article and public arXiv manuscript

Activity evidence

The identity controls scaling relations for gap, force, and overlap exponents in a heavily studied theory of jamming.

The theorem is conditional on the fullRSB scaling framework and takes existence and uniqueness of the relevant profile as given. Within that framework it closes the analytic identity.

Proof manuscript Journal publication

Previously numerical identity proved

System: Claude Sonnet 4.6 + Claude Opus 4.7
Verification: Author verified and journal published
Open for: Unproved since the 2014 fullRSB analysis
Research activity: 4/5

20 Feb 2026Automorphic forms and representation theory

First Proof Problem 2 — uniform Whittaker test vector

Problem statement

Does there exist one Whittaker-model vector

W

for

\mathrm{GL}_{n+1}(F)

that yields a finite, nonzero local Rankin–Selberg integral for every generic representation

\pi

\mathrm{GL}_n(F)

and every

s\in\mathbb C

OpenAI initially described its submission as likely correct, then withdrew that assessment after the official commentary and community analysis exposed a false support condition for a Whittaker vector.

Details and sources

AI contribution

The model identified a promising test vector and the key nonvanishing reduction, but its proposed support condition contradicts the representation’s central character.

Verification

Error documented by problem authors and acknowledged by OpenAI

Claim audit

The attempted “standard Howe-vector existence result” imposes support properties that cannot hold because they conflict with the vector’s central character.

Publication

OpenAI submission, official First Proof solutions, and author commentary

Activity evidence

A specialized research question whose public failure analysis illustrates how plausible local representation-theoretic arguments can break.

First Proof Batch 1 had ten questions but no formal grading process. OpenAI currently identifies five other attempts—Problems 4, 5, 6, 9, and 10—as having a high chance of correctness, not as formally accepted solutions.

OpenAI correction and submissions Official First Proof Batch 1 record Author solutions and error commentary

Initially favored proof attempt withdrawn

System: OpenAI internal reasoning model
Verification: Error documented by problem authors and acknowledged by OpenAI
Claim audit: Issue documented
Open for: Solved-but-unpublished benchmark question
Research activity: 3/5

Jul 2026Extremal polynomials

Erdős Problem #1038 — polynomial lemniscates

Problem statement

Among all nonconstant monic polynomials

f

whose roots lie in

[-1,1]

, determine

\inf_f\left|\{x\in\mathbb{R}:|f(x)|<1\}\right|.

A July 2026 manuscript by Darvas, Peng, and Tao claims an exact extremal value and measure for the real length of a monic polynomial’s unit lemniscate.

Details and sources

AI contribution

The initial main argument was generated in a GPT-5.5 Pro solver–verifier framework, then substantially revised, checked, and packaged by the human authors.

Verification

Author-checked manuscript; official record open

Publication

Public manuscript, exact symbolic checks, and interval-arithmetic certificates

Activity evidence

A problem originating with Erdős, Herzog, and Piranian in 1958, with historic work and especially intense expert activity in 2025–26.

The manuscript includes exact symbolic checks and interval-arithmetic certificates, but the official Erdős Problems record still listed #1038 as open when checked on 25 July 2026.

Proof manuscript Official problem record Verification artifacts

Candidate exact determination

System: GPT-5.5 Pro
Verification: Author-checked manuscript; official record open
Open for: 68 years
Research activity: 4/5

19 May 2026Partial differential equations

Lower bounds for advection–diffusion

Problem statement

For mean-zero solutions of advection–diffusion equations on the two-dimensional torus, derive explicit constructive lower bounds that rule out excessively fast mixing in three regimes: inviscid shear, diffusive shear, and rapidly oscillating time-periodic incompressible flows.

QED proved a polynomial lower bound for inviscid shears, a uniform positive mixing-scale lower bound for diffusive shears, and an exponential lower bound for rapidly oscillating time-periodic flows.

Details and sources

AI contribution

The system generated the complete chains of estimates without PDE-specific guidance; the most difficult case combined Floquet theory with techniques from other areas.

Verification

Domain expert verified

Publication

Dedicated arXiv paper, public proof records, and expert comments

Activity evidence

These were new questions from an expert’s active PDE research; one was estimated to require months or a year of human work and the resulting package was judged journal-level.

This record groups three closely linked questions from one research project. The expert judged the combined work suitable for journals such as JDE or SIAM Journal on Mathematical Analysis.

Research paper Proof and expert record QED system paper

Three research questions proved

System: QED / GPT-5.4 and GPT-5.5
Verification: Domain expert verified
Open for: Under 1 year
Research activity: 3/5

5 Mar 2026Mathematical physics

Cosmic-string radiation integral

Problem statement

Evaluate, for arbitrary loop angle

\alpha

and integer harmonic

N

I(N,\alpha)=\int_{S^2}\frac{[1-(-1)^N\cos(N\pi e_1)][1-(-1)^N\cos(N\pi e_2)]}{(1-e_1^2)(1-e_2^2)}\,d\Omega,

the singular integral determining the cosmic-string radiation power

P_N=32G\mu^2 I(N,\alpha)/(\pi^3N^2)

A Gemini Deep Think tree-search system derived six analytical methods for the singular sphere integral governing the harmonic power spectrum of gravitational radiation from arbitrary cosmic-string loop geometries.

Details and sources

AI contribution

The model proposed symbolic derivations while executable high-precision numerical feedback pruned erroneous branches across roughly 600 candidates.

Verification

Analytical derivation + numerical checks

Publication

Detailed arXiv manuscript with prompts, search constraints, code, and derivations

Activity evidence

A live mathematical-physics calculation with recent partial attempts, rather than a decades-old named conjecture.

Previous work had only asymptotic or odd-harmonic results. The paper gives a unified exact treatment and six independent derivation routes, but it has not been proof-assistant formalized.

Research paper

Exact analytical solution derived

System: Gemini Deep Think + tree search
Verification: Analytical derivation + numerical checks
Open for: Under 1 year
Research activity: 2/5

24 Feb 2026Matrix analysis

Ran–Teng Conjecture 20

The exact nonreal spectral region is determined for a four-cycle family of row-stochastic nonnegative matrices, resolving Conjecture 20 of Ran and Teng.

Details and sources

AI contribution

Seven model threads generated candidate reductions and proof components; the human authors selected, corrected, and closed the argument.

Verification

Human-checked mathematical proof

Publication

Detailed arXiv preprint; no formal proof assistant artifact located

This is a human–AI collaboration rather than a one-shot autonomous solution. The paper explicitly separates the model’s useful structural ideas from gaps repaired during correctness review.

Preprint and model record

Resolved in preprint

System: GPT-5.2 Thinking
Verification: Human-checked mathematical proof

24 Mar 2026Polynomial analysis

Erdős Problem #1153

Problem statement

For arbitrary interpolation nodes in

[-1,1]

, must the Lebesgue function on every fixed subinterval attain at least

(2/\pi-o(1))\log n

A sixty-five-year-old problem of Erdős and Turán concerning polynomials was resolved through sustained human–AI collaboration.

Details and sources

AI contribution

Program search, language models, and human mathematicians contributed complementary experimental and proof components.

Verification

Community-accepted proof

Publication

Public problem record and collaboration history

Activity evidence

1 cited source record and 1 problem-page discussion comment were located. The score is a conservative proxy for documented research attention.

This is a full resolution, but the provenance is distributed across tools and participants rather than a single model output.

Problem record Community AI ledger

Fully resolved

System: AlphaEvolve + Claude + Gemini Pro + GPT-5.2/5.4
Verification: Community-accepted proof
Open for: 65 years
Research activity: 1/5

20 Jan 2026Analysis

Effective Brascamp–Lieb inequalities

The Numina-Lean-Agent paper reports a successful Lean formalization of a Brascamp–Lieb theorem through interactive human–agent proof engineering.

Details and sources

AI contribution

A general coding agent interacted with Lean, retrieval tools, and human experts to build the formal development.

Verification

Paper report; complete source not located

Publication

Public system paper and agent repository; no complete Brascamp–Lieb source located in the linked repository

This is an author-reported autoformalization milestone for an established theorem, not a newly discovered mathematical resolution. The public paper’s displayed Lean excerpt still ends in `sorry`, so this index does not label it independently verified.

Research paper Agent and proofs

Author-reported formalization

System: Numina-Lean-Agent / Claude Opus 4.5
Verification: Paper report; complete source not located

9 Apr 2026Analysis, Discrepancy

Erdős Problem #987

Problem statement

For an infinite sequence

x_j\in(0,1)

, must the limsup exponential-sum amplitudes

A_k

be unbounded as

k\to\infty

? Can one at least have

A_k=o(k)

The problem was proved after remaining open for 62 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

OpenAI internal model is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

3 cited source records and 7 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: OpenAI internal model
Verification: Erdős Problems site confirmed
Open for: 62 years
Research activity: 2/5

9 Apr 2026Analysis

Erdős Problem #990

Problem statement

Can the angular discrepancy of the roots of a sparse complex polynomial be bounded by a constant times

\sqrt{n\log M}

, where

n

is its number of nonzero coefficients and

M

its normalized coefficient mass?

The problem was disproved after remaining open for 62 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

OpenAI internal model is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 1 problem-page discussion comment were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Conjecture disproved

System: OpenAI internal model
Verification: Lean checked
Open for: 62 years
Research activity: 1/5

31 Mar 2026Analysis, Discrepancy, Primes

Erdős Problem #997

Problem statement

For every real

\alpha

, is the sequence of fractional parts

\{\alpha p_n\}

along the primes necessarily not well-distributed in the strong sliding-window sense?

The problem was proved after remaining open for 62 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

OpenAI internal model is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: OpenAI internal model
Verification: Lean checked
Open for: 62 years
Research activity: 1/5

19 Apr 2026Analysis, Number Theory

Erdős Problem #1195

Problem statement

Let

S\subset\mathbb R

have infinite measure and suppose

x/y

is never an integer for distinct

x,y\in S

. How fast can

|S\cap(0,x)|

tend to infinity?

The problem was resolved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.4 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

Independent constructions by Haight and Szemerédi, followed by a quantitative question.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: GPT-5.4 Pro
Verification: Erdős Problems site confirmed
Open for: 46 years
Research activity: 3/5

21 Jun 2026Analysis

Erdős Problem #1197

Problem statement

For a positive-measure set

E\subset(0,\infty)

, let

E'=\bigcup_{r\geq1}rE

. Is it true that for almost every

x

there is

M(x)

such that

nx\in E'

for every integer

n>M(x)

The problem was disproved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Aristotle, Claude Opus 4.7, GPT-5.4 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

Specialist Haight question with limited documented follow-up.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Conjecture disproved

System: Aristotle, Claude Opus 4.7, GPT-5.4 Pro
Verification: Lean checked
Open for: 46 years
Research activity: 2/5

Combinatorics

22 Jul 2026Distance spectra of graphs

Graffiti Conjecture 284

Problem statement

If a finite graph

G

has girth at least five, must its minimum dual degree satisfy

\delta^*(G)\leq-\partial_n(G)

, where

\partial_n(G)

is the smallest eigenvalue of its distance matrix?

The Hoffman–Singleton graph is an exact counterexample: its minimum dual degree is 7 while the negative of its smallest distance-matrix eigenvalue is 4, so the conjectured inequality would require 7 ≤ 4.

Details and sources

AI contribution

A Capy research agent running Grok 4.5 Medium selected the conjecture, connected it to the Hoffman–Singleton graph, and produced the counterexample during an eight-minute agent run.

Verification

Exact certificate independently reproduced

Publication

Public agent transcript, independent integer-only verification, code, and artifact ledger

Activity evidence

A 1996 Graffiti conjecture recorded as open in a 2014 distance-spectra survey and again in a 2024 computational study.

The result is not yet a peer-reviewed journal publication. Its finite certificate has nevertheless been independently reproduced using exact integer matrix arithmetic and a second construction of the Hoffman–Singleton graph.

Capy agent transcript Independent exact verification Public announcement

Conjecture disproved

System: Grok 4.5 Medium / Capy Build
Verification: Exact certificate independently reproduced
Open for: 30 years
Research activity: 3/5

2 Feb 2026Graph polynomials and statistical physics

Multivariate independence-polynomial lower bound

Problem statement

Can the known degree-sensitive lower bound for the hard-core partition function be extended from one common activity to arbitrary nonnegative vertex fugacities?

Lee and Seo prove a degree-sensitive lower bound for the multivariate independence polynomial at arbitrary nonnegative vertex fugacities, extending the known univariate theorem and yielding a stronger two-color inequality.

Details and sources

AI contribution

The authors report that key technical steps were obtained with a custom Gemini Deep Think research agent, Aletheia, before the argument was completed and checked as a conventional paper.

Verification

Author-checked preprint

Publication

Complete public arXiv proof

Activity evidence

Independence polynomials and hard-core partition functions are central objects in an active combinatorics and statistical-physics literature.

The result generalizes the Sah–Sawhney–Stoner–Zhao lower bound from a common activity to vertex-dependent fugacities.

Research paper

General lower bound proved

System: Gemini Deep Think / Aletheia
Verification: Author-checked preprint
Research activity: 4/5

25 Mar 2026Hamiltonian graph decompositions

Hamilton decompositions of the directed 3-torus

Problem statement

For

D_3(m)=\vec C_m\square\vec C_m\square\vec C_m

, can the full arc set be partitioned into three directed Hamilton cycles for every integer

m\geq3

The directed product of three $m$ -cycles is decomposed into three arc-disjoint directed Hamilton cycles for every integer $m\geq3$ .

Details and sources

AI contribution

Claude first supplied the odd-order construction; later human–AI work handled even orders, unified the proof, and produced a Lean development.

Verification

Lean 4 formalization

Publication

Public arXiv proof, certificates, and Lean source

Activity evidence

The question prompted several independent constructions, a long unified proof, computational certificates, and a complete formalization in a short period.

This is the full directed 3-torus theorem. It is distinct from the narrower LEAP/Knuth subproblem already indexed elsewhere.

Unified research paper Lean development Knuth’s discovery account

All dimensions in the family proved

System: Claude Opus 4.6 / GPT-5.3 Codex / GPT-5.4 Pro
Verification: Lean 4 formalization
Open for: Newly posed in 2026
Research activity: 4/5

2 May 2026Ramsey theory

Ramsey numbers for book graphs

Problem statement

Does every

n

admit a graph on

4n-2

vertices containing no book

B_{n-1}

whose complement contains no

B_n

, and hence prove

R(B_{n-1},B_n)=4n-1

An AI scaffold found two additional infinite families and constructions for every remaining case through $n=56$ . The general equality $R(B_{n-1},B_n)=4n-1$ remains open.

Details and sources

AI contribution

GPT models supplied the core mathematical search while Claude Code implemented the search program; Epoch records the results and subsequent review.

Verification

Exact construction checks

Publication

Epoch open-problem page, write-up, and verifier

Activity evidence

A specialist Ramsey problem with a 1978 bound, modern infinite families, and several serious AI-assisted construction searches.

A later Dualverse system proposed another infinite family, but Epoch describes that output as under review; it is not counted here as a verified full result.

Epoch problem and progress record

New families and finite cases

System: GPT-5.2 Pro / GPT-5.4 Pro / Claude Code
Verification: Exact construction checks
Open for: Upper bound known since 1978
Research activity: 3/5

16 Mar 2026Ramsey theory

Diagonal Ramsey upper-bound constant

Problem statement

Within the stated diagonal-Ramsey ansatz, choose a correction polynomial and auxiliary functions satisfying all sufficient inequalities while minimizing the resulting constant

c=e^{F(1)}

Within the specified Gupta–Ndiaye–Norin–Wei ansatz, GPT-5.4 Pro proposed a correction reducing the automatically validated constant from about $3.7992$ to $3.6961$ .

Details and sources

AI contribution

The model proposed a quintic correction and piecewise auxiliary functions; the benchmark checked the sufficient inequalities using interval arithmetic.

Verification

Interval checked; expert review pending

Publication

HorizonMath paper and open verification framework

Activity evidence

Diagonal Ramsey numbers are a long-running international topic, though this record concerns one narrow optimization within a recent upper-bound framework.

This improves a constant inside a particular proof framework. HorizonMath labels the contribution as pending expert review, so the entry remains partial.

HorizonMath paper

Certified constant improved

System: GPT-5.4 Pro
Verification: Interval checked; expert review pending
Open for: Current optimization frontier
Research activity: 4/5

21 May 2026Ramsey theory

Erdős Problem #138 — gaps between van der Waerden numbers

Problem statement

W(k)

is the least

N

such that every two-colouring of

[1,N]

has a monochromatic

k

-term arithmetic progression, must

W(k+1)-W(k)\to\infty

AlphaProof Nexus proves $W(k+1)-W(k)\to\infty$ for the two-colour van der Waerden numbers. The stronger parent question $W(k)^{1/k}\to\infty$ remains open.

Details and sources

AI contribution

The system found a greedy extension argument for colourings and formalized the complete proof.

Verification

Lean checked

Publication

AP Nexus preprint and public Lean source

Activity evidence

Van der Waerden-number growth has a broad and long-running literature; this particular asymptotic gap variant is narrower.

The theorem is a separately recorded difference variant on the official problem page, not a full solution to Erdős #138.

Official problem record Formal statement Lean proof

Long-standing variant proved

System: AlphaProof Nexus
Verification: Lean checked
Open for: 45 years
Research activity: 4/5

21 May 2026Extremal graph theory

Written on the Wall II, Graph Conjecture 2

Problem statement

For a finite simple connected graph

G

, let

L_s(G)

be the maximum number of leaves in a spanning tree and

\ell(G)=|V(G)|^{-1}\sum_v\alpha(G[N(v)])

. Must

L_s(G)\geq2(\ell(G)-1)

For every finite connected graph, the maximum number of leaves in a spanning tree is at least twice the average local independence number minus two.

Details and sources

AI contribution

The system generated the proof and compiled a complete Lean formalization.

Verification

Lean checked

Publication

Public natural-language proof and Lean source

Activity evidence

Part of the long-running Graffiti conjecture program, with a specialist literature on spanning-tree leaves and local independence.

This is Conjecture 2 from the 1996 Written on the Wall II / Graffiti collection.

Formal statement and proof Lean source AP Nexus paper

Conjecture proved

System: AlphaProof Nexus
Verification: Lean checked
Open for: 30 years
Research activity: 3/5

21 May 2026Higher-order Fourier analysis

Ben Green’s Open Problem 57

Problem statement

For a finite abelian group

G

, let

\Phi(G)

be the absolutely convex hull of the specified trilinear kernels and let

\Phi'(G)

restrict the third factor to depend only on

x_1+x_2

. Is

\Phi(G)=\Phi'(G)

A counterexample over $G=\mathbb Z/3\mathbb Z$ separates the two absolutely convex hulls in Green’s question, with the strict support-function gap certified in Lean.

Details and sources

AI contribution

After an initial real-valued result and clarification of the intended complex formulation, numerical search found a candidate and the agent produced its rigorous proof.

Verification

Lean checked

Publication

AP Nexus preprint and public formal proof

Activity evidence

A young but technically serious item on a prominent 2024 open-problem list in additive combinatorics.

The clarification step matters: the final certificate addresses the intended complex-valued question, not only the easier real variant.

Green’s open-problem list Formal statement Lean proof

Intended complex form disproved

System: AlphaProof Nexus
Verification: Lean checked
Open for: 2 years
Research activity: 3/5

14 Jul 2026Enumerative combinatorics

Record compositions of alternating permutations

Problem statement

Can the record-partition enumeration for alternating permutations be refined to ordered record compositions, and does it admit a natural lift to noncommutative symmetric functions?

The ordered refinement is counted by an explicit product formula, and a canonical noncommutative-symmetric-function lift is constructed together with a broader exponential-seed generalization.

Details and sources

AI contribution

AxiomProver autonomously produced and Lean-verified the three main theorems answering the questions of Amdeberhan, Shareshian, and Stanley.

Verification

Lean checked

Publication

Public arXiv paper and formal source

Activity evidence

A new specialist enumerative-combinatorics problem from an active group of researchers, without a long independent literature trail.

The problem was newly posed in 2026, so its importance is assessed by mathematical content rather than age.

Solution paper Formal source Original problem paper

Open problem solved

System: AxiomProver
Verification: Lean checked
Open for: Open for less than one year
Research activity: 2/5

20 May 2026Partition theory

Reciprocals of partition polynomials

Problem statement

For

\operatorname{sp}(\lambda,x)=\prod_i(1+x^{\lambda_i})

, what divisibility, coprimality, recurrence, irreducibility, and coefficient-shape properties hold after reducing sums of

1/\operatorname{sp}(\lambda,x)

over the standard partition families?

AxiomProver proves six of ten conjectures about reduced reciprocal sums over ordinary, binary, odd, and ternary partitions, and finds a counterexample to the printed binary log-concavity statement.

Details and sources

AI contribution

The system generated the proofs and counterexample; the response paper’s authors checked and organized the results.

Verification

Lean checked

Publication

Public response paper and Lean repository

Activity evidence

A newly published specialist family of ten concrete conjectures, with rapid formal follow-up but no long history.

Several irreducibility and shape questions remain open. This is therefore an umbrella partial result, not a full settlement of the ten-conjecture family.

Response paper Original conjectures Formal artifacts

Six conjectures proved; one corrected

System: AxiomProver
Verification: Lean checked
Open for: Resolved within days of publication
Research activity: 2/5

21 May 2026Graph reconstruction

Weak bipartite reconstruction with distinct vertex types

Problem statement

If a suitably 2-connected bipartite graph has distinct vertex types

\tau(v)=(\deg v,\{\!\{\deg u:u\sim v\}\!\})

, is it determined up to bipartite isomorphism by the multiset of incidence-deletion cards?

A 2-connected bipartite graph is reconstructed from its incidence-deletion deck under an explicit strong condition that all degree-and-neighbour-degree vertex types are distinct.

Details and sources

AI contribution

AlphaEvolve helped formulate the reconstruction algorithm; AlphaProof Nexus proved its correctness under the distinct-type hypothesis.

Verification

Lean checked

Publication

AP Nexus paper and public Lean source

Activity evidence

The parent reconstruction program has more than sixty years of international attention, while this distinct-type theorem is narrowly scoped and new.

This is a strong-hypothesis variant. It does not solve the general graph reconstruction conjecture or the unrestricted bipartite problem.

Exact theorem and proof Lean proof

Restricted reconstruction theorem

System: AlphaEvolve / AlphaProof Nexus
Verification: Lean checked
Open for: New restricted variant
Research activity: 4/5

7 May 2026Critical graph theory

Erdős Problem #1032 — minimum degree in 4-critical graphs

Problem statement

Do arbitrarily large 4-chromatic edge-critical graphs exist with minimum degree bounded below by a positive constant times the number of vertices?

A new density–degree inequality implies $\delta(G)\leq(3/10+o(1))|V(G)|$ for 4-critical graphs, improving the previous coefficient $0.328$ . The existence of a positive linear lower construction remains open.

Details and sources

AI contribution

GPT-5.5 Pro with a research harness generated the note; Codex with the same harness produced the Lean development.

Verification

Lean checked + expert screening

Publication

Public note, formal proof, and official discussion

Activity evidence

A long critical-graph literature involving Simonovits, Toft, and a substantial 2023 advance.

The new inequality narrows the feasible range but does not answer Erdős’s existence question.

Official problem record Research discussion and artifacts

Upper obstruction improved

System: GPT-5.5 Pro / Codex
Verification: Lean checked + expert screening
Open for: At least 53 years
Research activity: 4/5

21 Jun 2026Discrepancy theory

Erdős Problem #176 — discrepancy on arithmetic progressions

Problem statement

Let

N(k,\ell)

be the least

N

such that every

f:[N]\to\{-1,1\}

has a

k

-term arithmetic progression

P

with

|\sum_{n\in P}f(n)|\geq\ell

. In particular, is

N(k,2)\leq C^k

A formal proof gives a polynomial upper bound for $N(k,2)$ , stronger than Erdős’s requested exponential bound. The broader two-parameter discrepancy problem remains open.

Details and sources

AI contribution

The repository author reports assistance from Codex 5.5 and ChatGPT 5.5 Pro while preparing the construction and its Lean formalization.

Verification

Public Lean proof

Publication

Official discussion and Lean repository

Activity evidence

Repeated in many Erdős sources since 1965 and closely tied to van der Waerden numbers and arithmetic-progression discrepancy.

The AI community ledger retains a cautious candidate-partial label, so the site does not promote the multipart parent problem to resolved.

Official problem record Research discussion Lean repository

The N(k,2) clause proved

System: Codex 5.5 / ChatGPT 5.5 Pro
Verification: Public Lean proof
Open for: 61 years
Research activity: 4/5

26 May 2026Extremal graph theory

Pentagons in triangle-free graphs

Problem statement

Does every triangle-free graph on

5n

vertices contain at most

n^5

copies of the five-cycle

C_5

The known affirmative theorem now has an AI-assisted, kernel-checked Lean proof.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

5 Feb 2026Combinatorial number theory

Distinct consecutive sums of permutations

Problem statement

For a permutation of

1,\ldots,n

, must the number of distinct sums of consecutive terms always be

o(n^2)

A counterexample to the conjecture was encoded and verified in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

24 May 2026Graph cycles

Cycle lengths in arithmetic progressions

Problem statement

Must every graph of sufficiently large average degree contain a cycle whose length lies in any prescribed infinite arithmetic progression containing even integers?

The affirmative theorem was reconstructed and checked in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Canonical Lean status; durable source not located

Publication

Official problem and discussion record

The canonical record labels the theorem Lean-verified, but this audit did not locate a durable public source file. The discussion thread is retained for provenance.

Problem, history, and proof record Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle / Claude Opus 4.7 / GPT-5.5
Verification: Canonical Lean status; durable source not located

7 Feb 2026Extremal graph theory

Triangle-free graph completion to diameter two

Problem statement

For every

\epsilon,\delta>0

and all sufficiently large

n

, can every triangle-free

n

-vertex graph with maximum degree

<n^{1/2-\epsilon}

be made triangle-free of diameter

2

by adding at most

\delta n^2

edges?

The known affirmative result now has a checked Lean formalization.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

31 Mar 2026Graph enumeration

Growth rate of minimal graph cuts

Problem statement

Does the exponential growth limit for the maximum number of minimal cuts in an

n

-vertex graph exist, and is it strictly below

2

The affirmative theorem and strict upper bound were formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

6 Feb 2026Additive combinatorics

Equidistribution of dense Sidon sumsets

Problem statement

A\subseteq\{1,\ldots,N\}

is a Sidon set with

|A|\sim N^{1/2}

, must

A+A

be well-distributed over all small moduli?

A proof exposition produced with ChatGPT was converted into a checked Lean development.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: ChatGPT / Aristotle
Verification: Lean checked

21 Apr 2026Discrepancy theory

Countable simultaneous discrepancy

Problem statement

Given infinite sets

A_i=\{a_{i1}<a_{i2}<\cdots\}

, is there

f:\mathbb N\to\{-1,1\}

such that

\max_{m,1\leq i\leq d}|\sum_{j\leq m}f(a_{ij})|\ll_d1

for every

d\geq1

Beck's affirmative theorem was autoformalized and kernel checked.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

27 Feb 2026Euclidean Ramsey theory

Monochromatic collinear sets

Problem statement

For every

k\geq3

, is there a finite

A\subset\mathbb R^2

such that every two-coloring of

A

has a line containing at least

k

points of

A

, with all points of

A

on that line having the same color?

A construction based on Hales–Jewett was given a checked Lean proof.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle / Gemini 3 Flash
Verification: Lean checked

10 May 2026Arithmetic progressions in words

Abelian-square-free lattice walks

Problem statement

For which dimensions must every positive unit-coordinate lattice walk contain three vertices in arithmetic progression? The threshold is true through dimension three and false from dimension four onward.

Keränen's 1992 construction and dimension threshold were formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

15 Apr 2026Arithmetic progressions

Monotone progressions in an ordering of the reals

Problem statement

Must every linear ordering of

\mathbb R

contain a monotone

k

-term arithmetic progression? The conjecture already fails for

k=3

The Ardal–Brown–Jungić counterexample was reconstructed and checked in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

24 Feb 2026Arithmetic progressions

Progression-free sets and their complements

Problem statement

A\subset\mathbb R

contains no three-term arithmetic progression, must its complement contain an infinite arithmetic progression?

Baumgartner's negative construction was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

19 Jun 2026Additive combinatorics

Partitioning bounded-representation sets

Problem statement

Can every set with uniformly bounded additive representation count be partitioned into finitely many sets with a strictly smaller bound?

The Nešetřil–Rödl negative theorem was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: AxiomProver
Verification: Lean checked

31 Jan 2026Additive combinatorics

Difference collisions at square-root density

Problem statement

Must two sets with counting functions of order at least

\sqrt N

have infinitely many common nonzero differences?

Ruzsa's binary-digit counterexample was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

1 Jun 2026Set theory and infinitary combinatorics

Erdős Problem #501 — relative independence under a measure extension

Problem statement

If every

A_x\subset\mathbb R

is bounded with outer measure below

1

, must there be an infinite

X\subseteq\mathbb R

such that

x\notin A_y

whenever

x\neq y

are in

X

A short AI-assisted note proves a positive answer to the infinite independent-set question assuming a countably additive extension of Lebesgue measure to all subsets of the real line.

Details and sources

AI contribution

GPT-5.5 Pro assisted the author in finding and revising the relative consistency argument and its section inequality.

Verification

Author checked; community screening

Publication

Public repository and Erdős Problems discussion

Activity evidence

A long-running Erdős–Hajnal set-theoretic problem with classical independence results and modern discussion.

This is a conditional or relative-independence result, not a ZFC solution. The official problem page remains open.

Official problem and literature record AI-assisted note and discussion

Conditional independence result

System: GPT-5.5 Pro
Verification: Author checked; community screening
Open for: 65 years
Research activity: 3/5

27 Jun 2026Extremal graph theory

Erdős Problem #1033 — triangle degree-sum bound

Problem statement

If every graph on

n

vertices with more than

n^2/4

edges contains a triangle whose vertex degrees sum to at least

h(n)

, is

h(n)\geq(2(\sqrt3-1)-o(1))n

A public GPT-5.5 Pro conversation claims an explicit construction disproving the proposed asymptotic lower bound for the maximum guaranteed degree sum of a triangle.

Details and sources

AI contribution

The model generated the claimed construction in a public discussion linked from the problem page.

Verification

Single community claim; not incorporated

Claim audit

The official page remains OPEN and says that no partial or complete solution has been incorporated from the comments.

Publication

Official open-problem page and one-comment discussion

Activity evidence

A Bollobás–Erdős extremal graph problem with classical upper and lower bounds but only one recent AI-claim comment.

This is included as a claim-audit record so that the public evidence is searchable. It is not counted as a confirmed disproof.

Official problem and known bounds Claim and public discussion

Counterexample claimed

System: GPT-5.5 Pro
Verification: Single community claim; not incorporated
Claim audit: Issue documented
Open for: 44 years
Research activity: 3/5

23 Jul 2026Infinite hypergraph theory

Erdős Problem #593 — obligatory triple systems

Problem statement

Which finite triple systems occur in every triple system of uncountable chromatic number?

A finite triple system is claimed to occur in every uncountably chromatic triple system exactly when, after isolated vertices are removed, it is linear, every hyperedge-node of its Levi graph meets a bridge, and every Berge cycle is even.

Details and sources

AI contribution

ChatGPT assisted ideation, proof exploration, refinement, programming, and orchestration. Aristotle assisted the author in building the accompanying Lean development.

Verification

Lean checked end to end; not yet conventionally refereed

Publication

Revised arXiv manuscript and public Lean 4 development

Activity evidence

The classification builds on decades of work on obligatory subsystems, uncountable chromatic number, and finite hypergraph structure.

The revised manuscript says the imported interfaces are proved inside Lean and packages the result in a hypothesis-free theorem using only standard Mathlib axioms. Conventional external review remains separate.

Revised proof manuscript Lean development Official problem record Discussion thread

Claimed resolution; Lean checked end to end

System: ChatGPT + Aristotle
Verification: Lean checked end to end; not yet conventionally refereed
Open for: Public Erdős problem
Research activity: 4/5

23 Jul 2026Infinite hypergraph theory

Erdős Problem #1177 — exact avoidance spectra

Problem statement

For a finite forbidden triple system

G

, what exact uncountable chromatic cardinalities can occur among

G

-free triple systems, and how do those spectra interact?

The revised manuscript gives truth values yes, no, and yes to the problem’s three exact-cardinal avoidance questions and proves a complete spectrum dichotomy for every finite forbidden triple system.

Details and sources

AI contribution

ChatGPT assisted the mathematical search and manuscript development. Aristotle supported the full Lean formalization, including the transfinite calibration argument.

Verification

Lean checked end to end; not yet conventionally refereed

Publication

Revised arXiv manuscript and public Lean 4 development

Activity evidence

The exact-cardinal formulation connects classical infinite combinatorics with modern obligatory-subsystem results.

This shares a proof core with Problem #593 but answers a distinct three-part Erdős problem. The kernel certificate verifies the encoded theorem; novelty and exposition still await normal scholarly review.

Revised proof manuscript Lean development Official problem record Discussion thread

Claimed resolution; Lean checked end to end

System: ChatGPT + Aristotle
Verification: Lean checked end to end; not yet conventionally refereed
Open for: Public Erdős problem
Research activity: 4/5

12 Jun 2026Spectral graph theory

Graffiti Conjecture 143

Problem statement

For every connected graph, is the variance of its positive adjacency eigenvalues at most its order divided by its average distance?

Exact dumbbell-graph certificates refute the claimed bound on the variance of positive eigenvalues under both standard conventions for average distance.

Details and sources

AI contribution

The pipeline found counterexamples beyond earlier search horizons and produced exact spectral-isolation checks, an independent rebuild, and mutation tests.

Verification

Dual exact checker routes; not externally refereed

Publication

Public note, certificates, source provenance, and runnable checks

Activity evidence

The conjecture survived an early computational attack and a 2025 eight-algorithm search to order 100.

The smallest certified witness under both common average-distance conventions has 39 vertices. No general minimality below 37 vertices is claimed.

Proof note and verification summary Certificates and checkers Verification catalog and runnable checks Verification method and limitations

Conjecture refuted

System: Demonstrandum multi-agent pipeline
Verification: Dual exact checker routes; not externally refereed
Open for: Survived computational attacks since 1990–91
Research activity: 3/5

12 Jun 2026Spectral graph theory

Graffiti Conjecture 154 under the standard-deviation reading

Problem statement

For every connected graph, is the deviation of its adjacency eigenvalues at most its order divided by its average distance?

Exact lollipop-graph certificates refute the inequality when “deviation” means population standard deviation, under both common average-distance conventions.

Details and sources

AI contribution

The pipeline discovered large witnesses and supplied independently written exact checkers, an independent rebuild, and mutation tests.

Verification

Dual exact checkers; reading-sensitive; not externally refereed

Claim audit

The original word “deviation” is ambiguous. Only the standard-deviation interpretation is claimed refuted; the alternative mean-absolute-deviation reading survives these witnesses.

Publication

Public note, frozen source, certificates, and runnable checks

Activity evidence

The conjecture survived old and modern computational searches, with the first certified lollipop-family violations appearing above 100 vertices.

The result is deliberately reading-specific. These examples do not refute the mean-absolute-deviation interpretation.

Proof note and exact scope Certificates and checkers Verification catalog and runnable checks Verification method and limitations

One standard reading refuted

System: Demonstrandum multi-agent pipeline
Verification: Dual exact checkers; reading-sensitive; not externally refereed
Claim audit: Issue documented
Open for: Reading-sensitive Graffiti conjecture
Research activity: 3/5

12 Jun 2026Graph domination and zero forcing

TxGraffiti–Davila Conjecture 9

Problem statement

G

is connected, cubic, and diamond-free, must

Z(G)\leq\gamma(G)+2

A connected, cubic, triangle-free fourteen-vertex graph has zero-forcing number $Z=7$ and domination number $\gamma=4$ , violating $Z(G)\leq\gamma(G)+2$ .

Details and sources

AI contribution

The system produced an explicit graph and independent Python and Rust checkers that exhaustively certify both graph parameters.

Verification

Dual independent checkers; not externally refereed

Publication

Public certificate, checkers, frozen source, and write-up

Activity evidence

The conjecture connects two active graph invariants and complements a proved claw-free sibling theorem.

The data suggest an unbounded gap on a chain family, but the general lower bound needed for that stronger claim is not proved.

Original conjecture Certificate and independent checkers Verification catalog and runnable checks Verification method and limitations

Conjecture refuted

System: Demonstrandum multi-agent pipeline
Verification: Dual independent checkers; not externally refereed
Open for: Central open question in a 2024 preprint
Research activity: 3/5

12 Jun 2026Independence polynomials

Pandey parity conjecture for generalized Petersen graphs

Problem statement

For every

n\geq2k+1

, is the independence polynomial of

GP(n,k)

real-rooted if and only if

k

is even?

Exact Sturm counts and independent brute force show an even- $k$ example that is not real-rooted and odd- $k$ examples that are real-rooted.

Details and sources

AI contribution

The pipeline produced exact polynomial certificates, a clean-room Python checker, an independent Rust enumeration, and mutation tests.

Verification

Dual independent exact checks; not externally refereed

Publication

Public certificates, checkers, and frozen source

Activity evidence

A recent exact conjecture about real-rootedness and generalized Petersen graphs, with a small computational search space.

The counterexamples lie outside the numerical window tested in the original paper. Other log-concavity claims in that paper are not addressed.

Original conjecture Certificates and independent checkers Verification catalog and runnable checks Verification method and limitations

Both directions refuted

System: Demonstrandum multi-agent pipeline
Verification: Dual independent exact checks; not externally refereed
Open for: Uncorrected 2026 preprint conjecture
Research activity: 2/5

12 Jun 2026Extremal graph theory

Koch–Narayan Conjecture 1

Problem statement

For a bipartite graph without isolated vertices and with a unique minimum dominating set, does the proposed function

m(n,\gamma)

upper-bound the number of edges whenever

\gamma\geq2

and

n\geq3\gamma

A thirteen-vertex bipartite graph with domination number $4$ , a unique minimum dominating set, and $22$ edges exceeds the conjectured maximum of $21$ .

Details and sources

AI contribution

The system produced explicit graph certificates, two clean-room checkers, an exhaustive filter, and mutation tests.

Verification

Dual independent checkers; not externally refereed

Publication

Public certificates, checkers, source snapshot, and write-up

Activity evidence

A recent extremal graph conjecture with a finite certificate and a natural parameter family.

The $\gamma=3$ strip is not refuted, and the claimed smallest-order classification relies on one exhaustive C implementation even though the concrete witness has independent checks.

Original conjecture Certificates and independent checkers Verification catalog and runnable checks Verification method and limitations

Conjectured upper bound refuted

System: Demonstrandum multi-agent pipeline
Verification: Dual independent checkers; not externally refereed
Open for: Open conjecture in a 2025 preprint
Research activity: 2/5

12 Jul 2026Enumerative combinatorics

Elizalde–Luo $\{1132,3312\}$ pattern-avoidance conjecture

Problem statement

Is the number of nonnesting multiset permutations avoiding

1132

and

3312

equal to

3^n-3\cdot2^{n-1}+1

The number of nonnesting permutations of $\{1,1,\ldots,n,n\}$ avoiding both $1132$ and $3312$ is proved to be $3^n-3\cdot2^{n-1}+1$ for every $n\geq1$ .

Details and sources

AI contribution

The system developed several proof routes, independently audited two complete written proofs, checked ground truth in three implementations, and formalized the general theorem in Lean.

Verification

Lean checked end to end; not externally refereed

Publication

Public proof note, Lean project, enumerators, and audit logs

Activity evidence

A concrete conjecture in modern permutation-pattern enumeration, supported by substantial finite data before the proof.

The published source had checked the formula only through $n=8$ . The Lean theorem covers all $n$ with the project’s pinned containment conventions.

Original published conjecture Proof and verification overview Lean proof and supporting artifacts Verification catalog and runnable checks

Conjecture proved and Lean checked

System: Demonstrandum multi-agent pipeline
Verification: Lean checked end to end; not externally refereed
Open for: Published 2025 conjecture
Research activity: 3/5

8 Jul 2026Enumerative combinatorics

Kurkov’s Fubini-number sum conjecture

Problem statement

For the Fubini numbers

a(n)

, is

a(n)=\sum_{k=0}^{2^{n-1}-1}\mathrm{A284005}(k)

for every

n>0

A refined ordered-set-partition argument proves Kurkov’s 2018 identity expressing the Fubini number $a(n)$ as a sum of values of OEIS sequence A284005.

Details and sources

AI contribution

The system produced a self-contained combinatorial proof, exhaustive verification over all ordered set partitions through $n=8$ , and a mutation-tested checker through $n=20$ .

Verification

Audited proof + exhaustive checker; not externally refereed

Publication

Public proof note, checker, and source record

Activity evidence

A precise sequence identity with a natural ordered-partition interpretation and a seven-year public record.

The general proof is human-readable and audit-panel checked rather than proof-assistant certified. The finite computations support but do not replace the argument.

Original OEIS conjecture record Proof note and checker Verification catalog and runnable checks Verification method and limitations

OEIS conjecture proved

System: Demonstrandum multi-agent pipeline
Verification: Audited proof + exhaustive checker; not externally refereed
Open for: OEIS conjecture posted in 2018
Research activity: 2/5

8 Jul 2026Additive combinatorics

Erdős Problem #866 — eventual value of $h_4$

Problem statement

Estimate the least excess

g_k(N)

forcing

k

integers whose pairwise sums all lie in a dense subset of

\{1,\ldots,2N\}

; in particular, determine the corresponding positive variant

h_4(n)

A verification-first multi-agent paper proves $h_4(n)=4$ for every $n\geq331{,}777$ , improves global $h_4$ and $g_5$ bounds, and certifies 298 exact finite cells.

Details and sources

AI contribution

The workflow developed the mathematics, extended an upstream Lean formalization, and combined kernel proofs with two SAT engines and archived DRAT/LRAT certificates.

Verification

Headline theorems Lean checked; finite cells independently certified

Publication

Public draft, complete Lean project, SAT certificates, and release freeze

Activity evidence

The question goes back to Choi, Erdős, and Szemerédi in 1975 and connects density thresholds, additive configurations, formal proof, and exact SAT computation.

This determines the eventual constant for the positive $h_4$ variant and materially advances #866, but the database’s broader request to estimate $g_k(N)$ for general $k$ remains open.

Official problem record Paper, Lean proof, and certificate guide Frozen proof manuscript Verification method and limitations

Major parameter case resolved

System: Demonstrandum multi-agent pipeline
Verification: Headline theorems Lean checked; finite cells independently certified
Open for: Partial resolution of a broader Erdős problem
Research activity: 4/5

13 Jul 2026Graph coloring

Strong-majority $4$ -edge-coloring with at most two degree- $3$ vertices

Problem statement

Does every admissible graph admit a strong-majority edge-coloring with four colors, and in particular can the five-color bound be improved on mixed degree-

\{3,4\}

graphs?

Every finite simple graph with all degrees in $\{3,4\}$ and at most two degree- $3$ vertices has a strong-majority edge-coloring with four colors.

Details and sources

AI contribution

A multi-model campaign built and falsified candidate approaches, assembled the Lean infrastructure, and completed the new mixed-class theorem under a verification-first acceptance gate.

Verification

Lean checked end to end; not externally refereed

Publication

Public theorem page, versioned archive, Lean statements, and falsification evidence

Activity evidence

A new graph-coloring program with contemporaneous five-color progress, extensive exact census evidence, and a remaining combinatorial descent lemma.

The theorem reaches genuinely mixed degree- $\{3,4\}$ graphs, where the previous general bound was five. The case of arbitrarily many degree- $3$ vertices and the universal four-color conjecture remain open.

Theorem, scope, and audit record Prior five-color theorem Lean statements and rebuild instructions Verification method and limitations

New mixed-class theorem; full conjecture open

System: OpenAI reasoning model + Anthropic reasoning model + Aristotle
Verification: Lean checked end to end; not externally refereed
Open for: New partial theorem toward a 2026 conjecture
Research activity: 3/5

27 Apr 2026Sidon sets and additive combinatorics

Erdős Problem #43 — paired Sidon sets

Problem statement

If Sidon sets

A,B\subseteq\{1,\ldots,N\}

satisfy

(A-A)\cap(B-B)=\{0\}

, must

\binom{|A|}{2}+\binom{|B|}{2}\leq\binom{f(N)}{2}+O(1),

where

f(N)

is the largest Sidon-set size in

[N]

? If

|A|=|B|

, can the right side be improved by a fixed positive proportion?

Both questions have negative answers. A Barreto construction disproves the equal-size bound; the unrestricted bound fails as a consequence of GPT-5.5 Pro’s full solution of Erdős Problem #42.

Details and sources

AI contribution

GPT-5.5 Pro supplied the decisive #42 theorem. Aristotle and Claude helped formalize the separate Barreto construction used for the equal-size clause.

Verification

Site confirmed; component Lean proofs

Publication

Official Erdős Problems resolution record, discussion, and formal artifacts

Activity evidence

A prize-backed Sidon problem with multiple Erdős sources, classical extremal constructions, and active modern discussion and formalization.

The official #43 page marks the full problem disproved, but does not badge the combined implication itself as wholly Lean-verified. The formal status here therefore remains mixed.

Official problem record Discussion and formalization Decisive Problem #42 record

Both proposed bounds disproved

System: GPT-5.5 Pro / Aristotle / Claude
Verification: Site confirmed; component Lean proofs
Open for: 44 years
Research activity: 4/5

24 Mar 2026Extremal combinatorics

Ramsey-style hypergraph construction

Problem statement

Let

H(n)

be the largest number of vertices in a hypergraph with no isolated vertices and no partition of size greater than

n

. If

k_1=1

and

k_n=\lfloor n/2\rfloor+k_{\lfloor n/2\rfloor}+k_{\lceil n/2\rceil}

, prove that

H(n)\geq c\,k_n

for some constant

c>1

, already for

n=15

, and give a constructive algorithm.

GPT-5.4 Pro found a four-way frame construction proving a uniform constant-factor improvement over the known recurrence for H(n), beginning at n = 15. The contributor confirmed the argument and is preparing it for publication.

Details and sources

AI contribution

Kevin Barreto and Liam Price elicited the first solution. The model supplied the construction, proof, recurrence, and executable algorithm.

Verification

Contributor verified

Publication

Full transcript and proof write-up; journal paper in preparation

Activity evidence

The question arose from a 2019 research line. Epoch reports roughly 5–10 serious attempts and rates the result as moderately interesting.

This is the full general challenge, not merely the finite warm-up. Epoch later obtained independent solutions from Claude Opus 4.6, Gemini 3.1 Pro, and GPT-5.4.

Epoch solution record Full GPT-5.4 transcript Proof write-up

Problem solved

System: GPT-5.4 Pro
Verification: Contributor verified
Open for: 7 years
Research activity: 2/5

10 Jul 2026Graph theory

Cycle Double Cover Conjecture

Problem statement

Does every finite bridgeless graph have a collection of cycles in which every edge appears exactly twice?

A short argument claims that every finite bridgeless loopless multigraph has a cycle double cover. Independent graph theorists have since published expositions of the proof.

Details and sources

AI contribution

OpenAI reports that a 64-agent run produced the proof in under an hour; Codex assisted with the writeup.

Verification

Independent expert expositions

Publication

OpenAI proof note plus multiple arXiv expositions; not yet journal reviewed

Activity evidence

A central graph-theory conjecture with sustained work, many equivalent formulations, and broad expert attention.

The proof has moved beyond a bare announcement: expositions by Jim Geelen and Sang-il Oum treat the argument as a proof. No Lean or Rocq formalization was located for this index.

Proof note Full prompt Independent exposition

Proof released; archival review ongoing

System: GPT-5.6 Sol Ultra
Verification: Independent expert expositions
Open for: 53 years
Research activity: 5/5

14 Jul 2026Graph theory

Sabidussi compatibility conjecture

A proof establishes the compatibility conjecture for graph products attributed to Sabidussi, closing the problem in the formulation studied by the authors.

Details and sources

AI contribution

The authors report that Pro found the proof and Sol helped turn the argument into a polished manuscript.

Verification

Lean checked + author review

Publication

Public arXiv preprint with a companion Lean repository

The machine-checked development is strong evidence for the encoded theorem. As always, the accompanying paper is needed to audit the correspondence between the Lean statement and the historical conjecture.

Preprint Lean repository

Resolved in preprint

System: GPT-5.6 Pro + GPT-5.6 Sol
Verification: Lean checked + author review

5 Dec 2025Ramsey theory

Erdős Problem #124

Problem statement

For bases

3\leq d_1<\cdots<d_r

satisfying the stated reciprocal-sum condition, can every sufficiently large integer be represented as a sum of distinct powers of the

d_i

? Under a coprimality assumption, does the same remain true after forbidding all low powers?

Aristotle proved and formalized the literal formulation then displayed in the database, but historical evidence indicates that Erdős intended a stronger statement that remains open.

Details and sources

AI contribution

Harmonic’s theorem-proving system generated a Lean proof of the supplied formal statement.

Verification

Reported Lean proof; linked statement contains sorry

Claim audit

Statement fidelity: the Lean target captured a weaker formulation than the historically intended conjecture, and the public linked statement is not a complete proof artifact.

Publication

Community post-mortem and official problem record

Activity evidence

Several source references exist, but the AI proof addressed a weaker literal formulation.

The AI work addressed a weaker literal formulation, while the intended Burr–Erdős–Graham–Li problem remains open. The linked Formal Conjectures statement contains `sorry`, and no complete source file for the solved variant was located.

Formalization post-mortem Current problem record Discussion thread

Weaker written variant only

System: Aristotle
Verification: Reported Lean proof; linked statement contains sorry
Claim audit: Issue documented
Research activity: 2/5

14 May 2025Extremal combinatorics

AlphaEvolve mathematics portfolio

Evolution over LLM-generated programs improved best-known constructions across a portfolio of open problems, including a 593-point lower bound for the 11-dimensional kissing number.

Details and sources

AI contribution

Language models proposed executable constructions while an evolutionary loop and problem-specific evaluators selected improvements.

Verification

Executable checks + expert review

Publication

Public technical report and repository covering 67 problems

These are genuine record improvements, not complete solutions of the surrounding open problems. Reproducible programs offer a stronger audit trail than an announcement alone, but they are not proof-assistant certificates.

DeepMind announcement Mathematics portfolio Public problem repository

New bounds; parent problems open

System: AlphaEvolve / Gemini
Verification: Executable checks + expert review

17 Oct 2025Claim audit

GPT-5 “ten Erdős problems” claim

A public claim that GPT-5 had solved ten previously open Erdős problems was walked back after most examples were traced to existing literature or misclassified database entries.

Details and sources

AI contribution

The model retrieved or reconstructed relevant arguments, but the announcement overstated their novelty as new mathematical solutions.

Verification

Community audit contradicted claim

Claim audit

Novelty failure: the announcement treated known or misclassified results as newly solved open problems.

Publication

Original social post deleted; contemporary reporting and the community audit are public

The episode is retained as a negative control. Literature search can be mathematically useful, but reproducing a known solution is not the same as settling an open problem.

Contemporary reporting Community Erdős AI ledger

Novelty claim withdrawn

System: GPT-5
Verification: Community audit contradicted claim
Claim audit: Issue documented

14 Dec 2023Additive combinatorics

FunSearch cap-set constructions

LLM-guided program search found larger cap sets in several dimensions and new constructions for related combinatorial problems; it did not solve the general cap-set problem.

Details and sources

AI contribution

The model proposed short programs inside an evolutionary search loop, with deterministic evaluators scoring candidate constructions.

Verification

Peer reviewed + executable checks

Publication

Peer-reviewed Nature paper with public code and constructions

FunSearch is included because it established the modern pattern of AI-assisted mathematical discovery with machine-checkable outputs. Its achievements are improved examples and bounds, not a theorem resolving the full asymptotic question.

Nature paper DeepMind account Code and constructions

Construction records improved

System: FunSearch / Codey
Verification: Peer reviewed + executable checks

9 Jul 2026Additive combinatorics

Erdős–Szemerédi sum–product conjecture over $\mathbb R$

An autonomous pipeline produced seven correct and structurally different disproofs of the real sum–product conjecture in eight independent trials.

Details and sources

AI contribution

A three-stage agent asked the model for proof plans, complete arguments, and adversarial review without problem-specific mathematical hints.

Verification

Author checked + reproducible trials

Publication

Public arXiv preprint; journal review pending

The result concerns the conjecture over the real numbers. It should not be conflated with every finite-field or quantitative sum–product problem that shares the same name.

Preprint and released runs

Real-field conjecture disproved

System: GPT-5.5 Pro
Verification: Author checked + reproducible trials

2 Jun 2026Graph theory

Knuth Hamiltonian-decomposition subproblem

A verified result handles a key subproblem in Knuth’s challenge on Hamiltonian decompositions of even-order Cayley graphs; the full research program remains broader.

Details and sources

AI contribution

An agent decomposed the informal argument, searched Mathlib, and iteratively discharged the resulting Lean goals.

Verification

Lean checked

Publication

Public research paper describing the formal development

The entry is deliberately marked partial: it is a verified research-level component, not a claim that every Hamiltonian decomposition question posed by Knuth is solved.

LEAP paper Released LEAP artifacts Hamiltonian-cycle formalization

Key subproblem formalized

System: LEAP + foundation models
Verification: Lean checked

8 Dec 2025Extremal combinatorics

Erdős Problem #1026

Problem statement

For distinct real numbers

x_1,\ldots,x_n

, determine the maximum possible sum along a monotone subsequence.

A weighted monotone-subsequence problem was resolved through a combination of computation, pattern discovery, literature search, packing reformulation, and proof.

Details and sources

AI contribution

Different systems contributed numerical exploration, formal assistance, literature retrieval, and conjecture generation within a human-led collaboration.

Verification

Lean checked + expert synthesis

Publication

Detailed public exposition and direct Lean proof

Activity evidence

A classic extremal-sequence setting with substantial modern discussion around the precise formulation.

The final theorem emerged from many small AI and human contributions plus previously disconnected 2016–17 literature. The direct Lean proof is public.

Tao’s full account Problem record Lean proof

Resolved with stronger conclusion

System: Aristotle + GPT + Gemini + AlphaEvolve
Verification: Lean checked + expert synthesis
Open for: 54 years
Research activity: 3/5

27 Apr 2026Sidon sets

Erdős Problem #42

Problem statement

Let

M\geq 1

and

N

be sufficiently large in terms of

M

. Is it true that for every Sidon set

A\subset \{1,\ldots,N\}

there is another Sidon set

B\subset \{1,\ldots,N\}

of size

M

such that

(A-A)\cap(B-B)=\{0\}

A question on the extremal behavior of Sidon-type sequences was resolved in a human–AI collaboration and subsequently encoded in Lean.

Details and sources

AI contribution

GPT-5.5 Pro supplied the central proof with Harjas Sandhu; Codex and GPT systems later assisted formalization.

Verification

Lean checked + community review

Publication

Problem-site record and public formalization

Activity evidence

1 cited source record and 6 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The index follows the community ledger’s full-solution classification. The dedicated problem page should be consulted for the exact quantifiers and attribution.

Problem record Community AI ledger

Resolved and later formalized

System: GPT-5.5 Pro + Codex
Verification: Lean checked + community review
Open for: 31 years
Research activity: 1/5

21 Apr 2026Graph theory

Erdős Problem #610

Problem statement

How large can the clique-transversal number

\tau(G)

be for an

n

-vertex graph? In particular, is

\tau(G)\leq n-\omega(n)\sqrt n

, or even

n-c\sqrt{n\log n}

A graph-theoretic problem of Erdős, Gallai, and Tuza follows from a 2021 theorem of Joret, Micek, Reed, and Smid; an AI-produced note made the implication explicit.

Details and sources

AI contribution

GPT-5.4 Pro wrote out the short deduction from the published theorem. Aristotle encoded a related Lean argument, but treated the external theorem as an assumption.

Verification

Published theorem + expert site record

Claim audit

Incomplete formalization: the decisive external theorem is assumed, so the Lean artifact is conditional rather than end to end.

Publication

Official problem record, AI note, and discussion of the incomplete formalization

Activity evidence

3 cited source records and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The mathematical credit belongs to the 2021 literature. The available Lean file is not end-to-end verification because its key external input is left as an assumption.

Problem record Discussion and provenance Community AI ledger

Problem resolved from prior literature

System: Aristotle + GPT-5.4 Pro
Verification: Published theorem + expert site record
Claim audit: Issue documented
Open for: 29 years
Research activity: 2/5

9 Jun 2026Graph theory

Erdős Problem #619

Problem statement

For a connected triangle-free graph

G

n

vertices, is there a constant

c>0

such that fewer than

(1-c)n

added edges always suffice to make the diameter 4 while keeping the graph triangle-free?

A counterexample settled a graph-theoretic conjecture of Erdős, Gyárfás, and Ruszinkó.

Details and sources

AI contribution

Fable generated the counterexample and additional systems assisted with checking and Lean formalization.

Verification

Lean checked

Publication

Public problem record and formal proof

Activity evidence

2 cited source records and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The formal artifact certifies the encoded counterexample. The problem page remains the source of truth for the historical formulation.

Problem record Independent tracker entry Community AI ledger

Conjecture disproved

System: Claude Fable 5 + Codex + GPT-5.5
Verification: Lean checked
Open for: 28 years
Research activity: 2/5

3 Apr 2026Sidon Sets

Erdős Problem #152

Problem statement

For any

M\geq 1

, if

A\subset \mathbb{N}

is a sufficiently large finite Sidon set, must there be at least

M

sums

a\in A+A

for which neither

a-1

nor

a+1

lies in

A+A

The problem was proved after remaining open for 32 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

DeepMind prover agent is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: DeepMind prover agent
Verification: Lean checked
Open for: 32 years
Research activity: 1/5

17 Jan 2026Number Theory, Covering Systems

Erdős Problem #281

Problem statement

Let

n_1<n_2<\cdots

be such that, for any choice of classes

a_i\pmod{n_i}

, the uncovered integers have density zero. For every

\epsilon>0

, must some

k

make the uncovered density below

\epsilon

for every choice of the first

k

classes?

The conclusion already follows from results of Davenport–Erdős and Rogers. The 2026 AI work supplied an independent proof that was later formalized.

Details and sources

AI contribution

GPT-5.2 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 28 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The AI work recovered and formalized an implication of older literature; it did not establish the first historical solution.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Known theorem reconstructed

System: GPT-5.2 Pro
Verification: Lean checked
Open for: Known from prior literature
Research activity: 3/5

21 Apr 2026Combinatorics, Set Theory

Erdős Problem #603

Problem statement

If a family of countably infinite sets has no pair intersecting in exactly two elements, what is the fewest colours always sufficient to colour their union so that none of the sets is monochromatic?

The problem was resolved after remaining open for 39 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.4 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 2 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: GPT-5.4 Pro
Verification: Erdős Problems site confirmed
Open for: 39 years
Research activity: 1/5

16 Apr 2026Additive Combinatorics

Erdős Problem #741

Problem statement

A+A

has positive upper density, can

A

be split into

A_1\sqcup A_2

so that both

A_1+A_1

and

A_2+A_2

have positive upper density? Is there a basis

A

of order

2

such that every partition prevents both sumsets from having bounded gaps?

The problem was resolved after remaining open for 32 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

DeepMind prover agent is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: DeepMind prover agent
Verification: Lean checked
Open for: 32 years
Research activity: 1/5

3 May 2026Graph Theory, Chromatic Number

Erdős Problem #750

Problem statement

Does there exist an infinite-chromatic graph in which every

m

-vertex subgraph has an independent set of size at least

m/2-f(m)

for some

f(m)\to\infty

The problem was proved after remaining open for 32 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.5 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

2 cited source records and 1 problem-page discussion comment were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.5 Pro
Verification: Lean checked
Open for: 32 years
Research activity: 2/5

22 Apr 2026Number Theory, Sidon Sets, Additive Combinatorics

Erdős Problem #863

Problem statement

Compare maximal finite sets with at most

r

representations of each sum to maximal sets with at most

r

representations of each difference. Are their asymptotic constants unequal, and is the difference-set constant smaller?

GPT-5.4 Pro recognized that existing bounds imply the answer; the relevant construction was already known by 2002.

Details and sources

AI contribution

GPT-5.4 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The AI contribution is literature synthesis rather than the first proof.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Known bounds recognized

System: GPT-5.4 Pro
Verification: Erdős Problems site confirmed
Open for: Known by 2002
Research activity: 1/5

22 Jun 2026Number Theory, Additive Combinatorics

Erdős Problem #865

Problem statement

Is there a constant

C

such that every sufficiently large

A\subseteq[1,N]

of size at least

5N/8+C

contains distinct

a,b,c

for which

a+b

a+c

, and

b+c

also lie in

A

The problem was proved after remaining open for 54 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.5 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

3 cited source records and 1 problem-page discussion comment were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.5 Pro
Verification: Lean checked
Open for: 54 years
Research activity: 2/5

25 Feb 2026Number Theory, Additive Combinatorics, Ramsey Theory

Erdős Problem #966

Problem statement

For

k,r\geq2

, does there exist a set of integers with no nontrivial

(k+1)

-term arithmetic progression but whose every

r

-colouring contains a monochromatic

k

-term progression?

The 1975 source already reports Spencer’s proof. Aristotle supplied a new Lean proof of the known result.

Details and sources

AI contribution

Aristotle is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This is a formalization milestone rather than a new solution.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Known theorem formalized

System: Aristotle
Verification: Lean checked
Open for: Known by 1975
Research activity: 1/5

16 Jun 2026Graph Theory, Ramsey Theory

Erdős Problem #986

Problem statement

For every fixed

k\geq3

, is the off-diagonal Ramsey number

R(k,n)

bounded below by

n^{k-1}/(\log n)^{c(k)}

The problem was proved after remaining open for 79 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Claude, OpenAI internal model is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: Claude, OpenAI internal model
Verification: Erdős Problems site confirmed
Open for: 79 years
Research activity: 1/5

23 Apr 2026Graph Theory, Ramsey Theory

Erdős Problem #1014

Problem statement

For every fixed

k\geq3

, does

R(k,l+1)/R(k,l)\to1

l\to\infty

The problem was proved after remaining open for 55 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

OpenAI internal model is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: OpenAI internal model
Verification: Lean checked
Open for: 55 years
Research activity: 1/5

9 Apr 2026Graph Theory, Chromatic Number

Erdős Problem #1091

Problem statement

Must every

K_4

-free 4-chromatic graph contain an odd cycle with at least two diagonals? More generally, can local 3-colourability force odd cycles with arbitrarily many diagonals?

Voss proved the first question in 1982; an OpenAI internal model disproved the second question in 2026, completing the two-part record.

Details and sources

AI contribution

OpenAI internal model is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 2 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The official status is solved rather than proved because the two clauses have different outcomes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Two-part problem resolved

System: OpenAI internal model
Verification: Erdős Problems site confirmed
Open for: 50 years
Research activity: 1/5

28 Apr 2026Graph Theory, Chromatic Number

Erdős Problem #1092

Problem statement

If every

m

-vertex subgraph is the union of an

r

-colourable graph and a graph with at most

f_r(m)

edges, how large can

f_r

be while forcing the whole graph to be

(r+1)

-colourable? Is

f_r(n)\gg_r n

Rödl’s 1982 construction already disproved the conjecture. GPT-5.5 Pro supplied a later application and write-up.

Details and sources

AI contribution

GPT-5.5 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 2 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The 2026 contribution is a new exposition/application, not the first counterexample.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Known construction applied

System: GPT-5.5 Pro
Verification: Erdős Problems site confirmed
Open for: Known by 1982
Research activity: 1/5

23 Apr 2026Number Theory, Covering Systems

Erdős Problem #1190

Problem statement

For a finite family of distinct moduli

m<n_1<\cdots<n_k

whose residue classes can be chosen pairwise disjoint, determine the largest possible reciprocal sum

\sum_i1/n_i

m\to\infty

The problem was resolved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.4 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

Dedicated proof building on several earlier covering-system results.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: GPT-5.4 Pro
Verification: Lean checked
Open for: 46 years
Research activity: 3/5

Geometry & topology

16 Mar 2026Geometric optimization

Thin-triangle Kakeya optimization at 128 slopes

Problem statement

For the fixed slopes

a_i=i/128

, choose rational intercepts

b_i

minimizing the area of the union of the prescribed thin triangular neighborhoods of the lines

y=a_ix+b_i

GPT-5.4 Pro proposed rational intercepts for the fixed slopes $a_i=i/128$ that reduce the verified union area by about 8.44% relative to the stated baseline.

Details and sources

AI contribution

The model searched the structured space of intercepts; HorizonMath’s public checker validates the resulting rational construction.

Verification

Automatically checked; expert review pending

Publication

HorizonMath paper and open verification framework

Activity evidence

The parent Kakeya program is major, while this exact finite optimization instance is a narrower, automatically verifiable research target.

The authors explicitly call this a potential novel contribution pending expert review. It is an optimization advance, not a solution of the Kakeya conjecture.

HorizonMath paper

Best-known construction improved

System: GPT-5.4 Pro
Verification: Automatically checked; expert review pending
Open for: Current optimization frontier
Research activity: 3/5

Feb 2026Combinatorial geometry

Erdős Problem #652 — distinct distances from selected points

Problem statement

For planar points

x_1,\ldots,x_n

, let

R(x_i)

count the distinct distances from

x_i

and order these counts increasingly. If

\alpha_k

is the least constant permitting

R(x_k)<\alpha_k\sqrt n

in arbitrarily large configurations, must

\alpha_k\to\infty

Aletheia connected the question to Mathialagan’s 2021 theorem, which implies the required divergence. The contribution is a literature-based resolution rather than a newly invented proof.

Details and sources

AI contribution

The research agent searched the literature, matched the problem to an existing theorem, and produced a public solution record.

Verification

Official problem record updated

Publication

DeepMind paper, released output, and Erdős Problems record

Activity evidence

A documented combinatorial-geometry problem with a modest literature trail; the decisive theorem had already appeared in 2021.

This corrects the open-status record by applying known literature. It should not be read as a new 2026 theorem.

Official problem record Erdős case-study paper Aletheia system paper Released Aletheia outputs

Resolved through literature recovery

System: Aletheia / Gemini Deep Think
Verification: Official problem record updated
Open for: 29 years
Research activity: 2/5

Feb 2026Combinatorial geometry

Erdős Problem #654 — distinct distances with no four concyclic

Problem statement

n

planar points have no four concyclic, must some point determine

(1-o(1))n

distinct distances? Failing that, can one always force more than

(1/3+c)n

for some fixed

c>0

Aletheia constructed configurations in which every point sees at most about $3n/4$ distinct distances, refuting the proposed $(1-o(1))n$ lower bound. The weaker improvement beyond $n/3$ remains open.

Details and sources

AI contribution

The agent autonomously generated and revised the counterexample in DeepMind’s solver–verifier workflow.

Verification

Expert-reviewed project result

Publication

DeepMind paper, released output, and official problem discussion

Activity evidence

A decades-old distinct-distances problem connected to an active geometric-combinatorics literature, but narrower than the classical Erdős distinct-distances problem.

Only the strongest proposed asymptotic form is settled. The parent problem remains open and is therefore classified as partial.

Official problem record Erdős case-study paper Aletheia system paper Released Aletheia outputs

Strongest form disproved

System: Aletheia / Gemini Deep Think
Verification: Expert-reviewed project result
Open for: 39 years
Research activity: 3/5

28 Apr 2026Decision problems in topology

Kirby Problem 5.16 for noncommutative semifree DGAs

Problem statement

For semifree noncommutative differential graded algebras, are stable tame isomorphism, quasi-isomorphism, or derived Morita equivalence algorithmically decidable?

Over every nontrivial computable unital commutative ring, the released proofs show that stable tame isomorphism, quasi-isomorphism, and derived Morita equivalence are all undecidable for arbitrary semifree noncommutative DGAs.

Details and sources

AI contribution

Aletheia produced the public natural-language proof artifact; the repository identifies it as a resolution of Problem 5.16 in the stated noncommutative setting.

Verification

Human-checked public proofs

Publication

Dedicated public preprint and released raw outputs

Activity evidence

Kirby’s problem lists have broad standing in low-dimensional topology; this is a precise algebraic-decision subcase rather than the whole surrounding program.

The analogous graded-commutative formulations remain open. The scope qualifier is therefore essential.

Dedicated research paper Released Aletheia outputs

Specified case proved undecidable

System: Aletheia / Gemini Deep Think
Verification: Human-checked public proofs
Open for: K3 / Kirby problem-list question
Research activity: 3/5

3 Feb 2026Flat surfaces and moduli spaces

Spin parity for $k$ -differentials

Problem statement

For odd

k

and

\gcd(n,k)=\gcd(n+1,k)=1

, let

N_k(n)

count pairs

1\leq b_i\leq(k-1)/2

with

b_1+b_2\geq(k+1)/2

and

b_2\equiv nb_1\pmod k

. Is

N_k(n)\equiv\lfloor(k+1)/4\rfloor\pmod2

The parity identity conjectured by Chen and Gendron is proved for every odd $k$ under the stated coprimality assumptions, removing a conditional step in the genus-zero and genus-one spin-parity classification.

Details and sources

AI contribution

The system found a Jacobi-symbol reformulation and the key proof strategy; the central number-theoretic identity was then formalized in Lean.

Verification

Expert proof + Lean-checked core

Publication

Public preprint and Lean repository

Activity evidence

A focused conjecture in a sustained specialist program on strata of differentials, flat surfaces, and spin parity.

Lean checks the number-theoretic identity itself, not every downstream statement about moduli spaces.

Research paper Lean source

Number-theoretic conjecture proved

System: AxiomProver
Verification: Expert proof + Lean-checked core
Open for: 4 years
Research activity: 3/5

17 Feb 2026Discrete geometry

Distances in convex polygons

Problem statement

Must the vertices of every convex

n

-gon determine at least

\lfloor n/2\rfloor

distinct distances?

Altman's 1963 affirmative proof was formalized in Lean through a mixed agent workflow.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle / Claude Opus 4.5 / Claude Opus 4.6 / Gemini 3 Flash / Gemini 3 Pro / Numina Lean Agent
Verification: Lean checked

15 Jan 2026Discrete geometry

Convex-distance multiplicities

Problem statement

f(d)

counts pairs of vertices of a convex

n

-gon at distance

d

, is

\sum_d f(d)^2=O(n^3)

A stronger known theorem was given a public Lean proof, with independent AI proof work also recorded.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Codex / GPT-5.2 Thinking / Seed Prover 1.5
Verification: Lean checked

17 Nov 2025Combinatorial geometry

Lines through one planar point set

Problem statement

For disjoint planar sets

A

and

B

of sizes

n

and

n-3

, respectively, with not all of

A

contained on one line, must some line contain at least two points of

A

and no point of

B

Xichuan's three explicit counterexamples were reconstructed with GPT Pro and verified by Aristotle in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: ChatGPT Pro / Aristotle
Verification: Lean checked

17 Dec 2025Euclidean Ramsey theory

Monochromatic rectangles of prescribed area

Problem statement

\mathbb R^2

is finitely colored, must there be one color class containing the vertices of a rectangle of every positive area?

A negative construction was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle / Gemini 3 Pro
Verification: Lean checked

14 Jan 2026Discrete geometry

Obtuse angles among Euclidean points

Problem statement

Must every set of

2^d+1

points in

\mathbb R^d

contain three points forming an obtuse angle?

The classical affirmative theorem received a new AI-generated Lean proof.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Codex / GPT-5.2 Thinking
Verification: Lean checked

27 Dec 2025Discrete geometry

Distance multiplicities beyond lines and circles

Problem statement

Let

A\subset\mathbb R^2

have size

n

, let

d_1,\ldots,d_k

be its distinct distances, and let

f(d)

be the distance multiplicity. Is

k=n-1

and

\{f(d_i)\}=\{n-1,\ldots,1\}

equivalent to

A

being a set of equidistant points on a line or a circle?

Aristotle independently found the four-point counterexample and produced the public Lean proof.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

19 Jan 2026Geometric graph theory

Graphs of Euclidean dimension four

Problem statement

What is the minimum number of edges in a graph of Euclidean dimension four, and which graph attains it?

A Lean proof establishes the minimum as nine edges, uniquely attained by $K_{3,3}$ .

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

19 Jun 2026Combinatorial geometry

Ordinary triangles in line arrangements

Problem statement

For

d\geq4

, must every collection of

d

pairwise non-parallel lines in

\mathbb R^2

, with no point incident to four lines, contain three lines whose three intersection points are distinct and each incident to exactly two lines of the arrangement?

Escudero's counterexample to the conjecture was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: AxiomProver
Verification: Lean checked

2 Mar 2026Euclidean Ramsey theory

Unit-square Ramsey complement

Problem statement

S\subset\mathbb R^2

contains no pair of points at unit distance, must its complement contain the four vertices of a unit square?

Juhász's affirmative theorem was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

10 Jun 2026Discrete geometry and low-dimensional topology

Piecewise-affine Möbius-band width

Problem statement

For the benchmark's

G_\beta

-invariant clean triangulations and squeeze maps of the strip, prove that

\sqrt 3

is the infimum of the realized values of

\beta

Three systems proved the sharp threshold and received minor-revision decisions. Reviewers found the mathematics correct, while documenting missing attribution and an incorrect historical citation in some submissions.

Details and sources

AI contribution

Three independent GPT-5.5-Pro-based systems translated ideas around the optimal paper Möbius band into the benchmark's piecewise-affine setting.

Verification

Double-blind expert review; minor revisions

Publication

First Proof Second Batch report, complete submissions, logs, and referee reports

Activity evidence

The formulation is new, but it is rooted in the nearly fifty-year history of the sharp paper Möbius-band problem.

The benchmark problem is a new affine variant of the Halpern–Weaver problem. Reviewers emphasized that several solutions closely followed Schwartz's prior work without adequate attribution.

First Proof benchmark and source files Official report and referee decisions Problems, submissions, reviews, and logs

Research problem proved

System: GPT-5.5 Pro / ProofCouncil / UCLA Moonshot
Verification: Double-blind expert review; minor revisions
Open for: New variant of a 50-year problem
Research activity: 4/5

10 Jun 2026Lattice theory and low-dimensional topology

Irreducible vertices in definite tree lattices

Problem statement

Let

T

be a positive-definite weighted tree with exactly one vertex

v

satisfying

w(v)<d(v)

. Must

T

contain a vertex that is irreducible in its lattice

L(T)

The UCLA Moonshot harness and ChatGPT 5.5 Pro produced complete proofs. All three referees assigned to each submission found the arguments mathematically correct and essentially flawless.

Details and sources

AI contribution

A one-shot harness and the base model independently reconstructed the tree-lattice argument used in work toward the Neumann–Zagier conjecture.

Verification

Three expert referees; essentially flawless

Publication

First Proof Second Batch report, complete submissions, logs, and referee reports

Activity evidence

A specialized but technically serious problem connected to ongoing work on the Neumann–Zagier conjecture; the authors reported several months of effort.

The authors had a private proof after several months of work. Referees found the AI proofs complete but less conceptually organized than the human solution.

First Proof benchmark and source files Official report and referee decisions Problems, submissions, reviews, and logs

Research problem proved

System: GPT-5.5 Pro / UCLA Moonshot
Verification: Three expert referees; essentially flawless
Open for: Unpublished research lemma
Research activity: 3/5

10 Jun 2026Combinatorial topology

Contractibility of a crossing-matching complex

Problem statement

For a reducible quasi-reduced free-group word

w

, let

F_w

be the CW complex whose cells encode crossing matchings and their resolutions. Must

F_w

be contractible?

Every tested system found a counterexample. Two submissions were rated essentially flawless and the other two required only minor revisions.

Details and sources

AI contribution

Four independent systems recognized that the newly defined CW complex need not be contractible and supplied explicit topological counterexamples.

Verification

Double-blind expert review; all four passed

Publication

First Proof Second Batch report, complete submissions, logs, and referee reports

Activity evidence

A new technical object arising inside an active topology project, with little prior standalone literature.

The object was newly defined in work on a stable homotopy refinement of Legendrian contact homology. This was a short-lived research conjecture rather than a longstanding public problem.

First Proof benchmark and source files Official report and referee decisions Problems, submissions, reviews, and logs

Conjecture disproved

System: ProofCouncil / UCLA Moonshot / ChatGPT 5.5 Pro / Momus with Gemini 3.1 Pro
Verification: Double-blind expert review; all four passed
Open for: Newly posed research conjecture
Research activity: 2/5

11 Jun 2026Polyhedral combinatorics

IRIS Conjecture 6.1 on simple $3$ -polytopes

Problem statement

For a simple

3

-polytope with at least three faces of size at least

7

, must

p_6\geq\frac{39}{20}+\frac{p_3}{2}-\frac{p_5}{4}-\sum_{k\geq7}p_k

Five minimal ten-face counterexamples refute the printed face-vector inequality. The simplest has $p_3=4$ , $p_5=3$ , $p_7=3$ , and $p_6=0$ .

Details and sources

AI contribution

A verification-first multi-agent search produced exact certificates, independently implemented Python and Rust checkers, a mutation suite, and a clean-room census.

Verification

Dual independent checkers; not externally refereed

Publication

Public certificates, checkers, frozen source, and write-up

Activity evidence

A recent AI-for-mathematics workshop conjecture with a finite polyhedral search space and no prior public correction located.

The integer-rounded weakening survives the census through sixteen faces, and no claim is made about the paper’s other conjectures.

Original conjecture record Certificates and independent checkers Verification catalog and runnable checks Verification method and limitations

Conjecture refuted as printed

System: Demonstrandum multi-agent pipeline
Verification: Dual independent checkers; not externally refereed
Open for: Open workshop-paper conjecture
Research activity: 2/5

11 Jun 2026Discrete geometry

Discrete Borsuk Conjecture 3

Problem statement

For bounded

S\subset\mathbb Z^d

, is

\beta_{\mathbb Z}(S)=2^d

if and only if

\operatorname{conv}(S)

is unimodularly equivalent to

[0,m]^d

A four-point set in $\mathbb Z^2$ has lattice Borsuk number $4=2^2$ but a convex hull containing seven lattice points, so it is unimodularly equivalent to no lattice square.

Details and sources

AI contribution

The pipeline found the witness, froze the source definitions, and built a complete Lean development with a statement-fidelity ledger and axiom audit.

Verification

Lean checked end to end; not externally refereed

Claim audit

Statement-reading caveat: the checked counterexample kills the published all-bounded-sets biconditional, while a plausible full-set repair remains open.

Publication

Public proof note, Lean project, and reproducible audit

Activity evidence

The problem is a discrete analogue of the Borsuk partition problem, with both geometric and formal-definition subtleties.

This refutes the conjecture exactly as printed. The unstated repair requiring $S=\operatorname{conv}(S)\cap\mathbb Z^d$ is not refuted by this witness.

Original conjecture Lean proof and fidelity audit Verification catalog and runnable checks Verification method and limitations

Printed biconditional disproved

System: Demonstrandum multi-agent pipeline
Verification: Lean checked end to end; not externally refereed
Claim audit: Issue documented
Open for: Published 2025 conjecture
Research activity: 3/5

21 Jul 2026Knot theory

Conant’s mod- $4$ Kawauchi conjecture

Problem statement

For every amphicheiral knot

K

, does there exist

f(z)\in\mathbb{Z}[z]

such that

\nabla_K(z)\equiv f(z)f(-z)\pmod 4\,?

Jim Conant proved the mod-4 factorization of the Conway polynomial for every amphicheiral knot with help from Claude Fable 5.

Details and sources

AI contribution

The paper credits Claude Fable 5 with helping produce the proof; no more granular discovery record was released.

Verification

Author-checked preprint

Publication

Complete public arXiv proof

Activity evidence

A meaningful specialist conjecture connected to a substantial literature on amphicheiral knots, Conway polynomials, and factorization obstructions.

This proves Conant’s 2006 congruence conjecture. It does not revive Kawauchi’s stronger integral factorization, which is false in general.

Research paper

Conjecture proved

System: Claude Fable 5
Verification: Author-checked preprint
Open for: 20 years
Research activity: 3/5

17 May 2026Algebraic geometry

Integral local invariant cycles in degree one

Problem statement

Let

X\to B

be a semistable one-parameter family of complex projective varieties, let

X_t

be a smooth nearby fiber, and let

T

act on

H^1(X_t,\mathbb{Z})

. Is the natural map

H^1(X,\mathbb{Z})\longrightarrow H^1(X_t,\mathbb{Z})^T

surjective?

QED found an independent proof that the integral local invariant cycle map is surjective in degree one for a semistable one-parameter degeneration, even though the integral statement fails in higher degree.

Details and sources

AI contribution

The system received only the statement and produced a proof mathematically different from the human author’s unreleased proof.

Verification

Domain expert verified

Publication

Public full proof, expert assessment, and comparison paper

Activity evidence

The rational invariant cycle theorem dates to the 1970s, but the exact integral degree-one question in the QED record was newly contributed in 2026.

The expert called the residue-theoretic idea original, elementary, elegant, and moderately difficult. This resolves degree one, not the false all-degrees integral analogue.

AI-generated proof QED system paper Human comparison paper

Degree-one theorem proved

System: QED / GPT-5.5
Verification: Domain expert verified
Open for: Newly posed in 2026
Research activity: 3/5

20 Jul 2026Algebraic geometry

Jacobian Conjecture

Problem statement

Does every polynomial map F: ℂⁿ → ℂⁿ with constant nonzero Jacobian determinant have a polynomial inverse?

An explicit polynomial map in three variables has constant nonzero Jacobian determinant but maps three distinct points to the same value. The two-variable case remains open.

Details and sources

AI contribution

Levent Alpöge credited Fable with finding the counterexample after Akhil Mathew suggested the question.

Verification

Lean checked

Publication

Public counterexample and expert expositions; no journal paper yet

Activity evidence

A major named conjecture with decades of international work, surveys, reductions, and specialist programs.

This is a complete disproof of the dimension-independent conjecture, not a solution of the still-open n = 2 case. The short explicit certificate can also be checked directly by symbolic algebra.

Original announcement Tao’s mathematical digestion Lean formalization

General conjecture disproved

System: Claude Fable 5
Verification: Lean checked
Open for: 87 years
Research activity: 5/5

11 Jul 2026Algebraic geometry

Grothendieck’s group-scheme question

Problem statement

Is every finite locally free group scheme of order n killed by n, without assuming that the group scheme is commutative?

A finite locally free group scheme of order four was constructed that is not killed by four, settling Grothendieck’s general noncommutative question by counterexample.

Details and sources

AI contribution

Under Akhil Mathew’s direction, Sol found the construction and Fable translated the argument into Lean.

Verification

Lean checked

Publication

Public, unmerged mathlib pull request and expert account; journal publication pending

Activity evidence

A specialist question of Grothendieck with a substantial surrounding group-scheme literature.

The 1,076-line Lean development was compiled and its statement audited against mathlib’s definitions, but the public pull request remained unmerged when checked. The commutative case, previously proved by Deligne, is not contradicted.

Lean development Expert account

Question answered negatively

System: GPT-5.6 Sol + Claude Fable 5
Verification: Lean checked
Research activity: 3/5

20 May 2026Discrete geometry

Erdős unit-distance conjecture

Problem statement

If u(n) is the maximum number of unit-distance pairs among n planar points, is u(n) = n^(1+o(1))?

An infinite family of planar point sets gives at least n^(1+δ) unit-distance pairs, disproving the expected n^(1+o(1)) upper bound. The exact extremal growth rate remains open.

Details and sources

AI contribution

OpenAI reports an autonomous proof from a general-purpose model, later digested and improved by human mathematicians.

Verification

Expert checked + Lean formalizations

Publication

Proof and nine-author companion remarks released publicly

Activity evidence

One of the best-known problems in discrete geometry, with a large literature and repeated improvements over eight decades.

The conjectured asymptotic upper bound is definitively false, but headlines saying the entire planar unit-distance problem is solved are too broad. Subsequent public reports describe both conditional and axiom-level Lean formalizations.

OpenAI announcement Proof Released reasoning record Formalization account

Central conjecture disproved

System: Internal OpenAI reasoning model
Verification: Expert checked + Lean formalizations
Open for: 80 years
Research activity: 5/5

19 Mar 2026Algebraic geometry

Simplicity of the Hodge bundle

For the moduli space of genus g ≥ 2 curves, the Hodge bundle was shown to contain no nontrivial sub-bundles.

Details and sources

AI contribution

The author supplied a single prompt asking for a proof and reports that the mathematical content came from the agent’s output.

Verification

Expert-authored and checked preprint

Publication

Public arXiv paper; no proof-assistant formalization located

The paper distinguishes mathematical generation from expository editing, but the proof remains human-reviewed rather than kernel checked.

Preprint and interaction card

Research question proved

System: Aletheia / Gemini Deep Think
Verification: Expert-authored and checked preprint

30 Jan 2026Arithmetic geometry

Eigenweights for arithmetic Hirzebruch proportionality

Previously unknown eigenweights in the higher arithmetic Hirzebruch proportionality formula were determined for all classical groups.

Details and sources

AI contribution

The agent connected arithmetic geometry to symmetric-group representation theory and derived the general formulas.

Verification

Domain-expert checked preprint

Publication

Public arXiv research paper

This is a computation of new structure constants within an existing theory, not a proof of the entire arithmetic proportionality principle.

Research paper Agent evaluation paper Prompt and model output

General eigenweights determined

System: Aletheia / Gemini Deep Think
Verification: Domain-expert checked preprint

7 May 2026Algebraic geometry

Minimal volume of rank-one stable surfaces

A human proof established the sharp lower bound 1/6351 and uniqueness of the minimizing surface; an AI chatbot re-derived a plurigenus inequality used as the decisive filter.

Details and sources

AI contribution

The model supplied a key inequality that the authors integrated with classification arguments and additional human mathematics.

Verification

Human proof in public preprint

Publication

Public arXiv paper; publication review ongoing

The theorem is a genuine resolution, but the AI contribution is one decisive ingredient rather than the complete proof. It is therefore classified as partial AI contribution.

Preprint

Decisive AI-derived step

System: AI chatbot, model not specified
Verification: Human proof in public preprint

12 Jan 2026Algebraic geometry

Motivic class of genus-zero maps to a flag variety

Under a mild positivity condition on the curve class, the motivic class of based genus-zero maps to the complete flag variety was computed through an iterative human–AI proof strategy.

Details and sources

AI contribution

AI systems solved scaffolded special cases; human analysis extracted the general mechanism, after which the systems completed remaining steps.

Verification

Multi-author mathematical proof

Publication

Public arXiv preprint

This case is included to avoid reducing AI mathematics to autonomous one-shot proofs: the result depended on an iterative division of labor.

Preprint

Human–AI proof completed

System: FullProof workflow
Verification: Multi-author mathematical proof

25 Feb 2026Discrete geometry

Erdős Problem #846

Problem statement

If every

n

-point subset of an infinite planar set contains at least

\epsilon n

points with no three collinear, must the whole set be a finite union of sets with no three collinear?

Independent AI efforts produced a counterexample and Lean proof; a 2024 result implying a comparable counterexample was identified afterward.

Details and sources

AI contribution

The DeepMind system produced a Lean-verified solution while an OpenAI model independently found an informal one.

Verification

Lean checked + independent derivation

Publication

Public problem record; comparable 2024 literature found afterward

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The entry records independent problem solving and formal verification, not the first historical proof of the negative answer.

Problem record Community AI ledger

Independent rediscovery formalized

System: DeepMind prover agent + OpenAI internal model
Verification: Lean checked + independent derivation
Open for: Known from 2024 literature
Research activity: 1/5

23 Feb 2026Discrete geometry

Sphere packing in dimensions 8 and 24

Viazovska’s dimension-8 proof and the dimension-24 Leech-lattice proof were completed as sorry-free Lean developments totaling roughly 200,000 lines.

Details and sources

AI contribution

Gauss worked from a substantial human blueprint and existing repository, then completed the remaining proof goals at scale.

Verification

Lean checked + expert project audit

Publication

Public repository, project site, and formalization paper

The mathematical theorems were proved in 2016. The 2026 milestone is formal verification, not a new solution of sphere packing.

Project site Formalization paper Gauss account

Fields Medal proofs formalized

System: Gauss
Verification: Lean checked + expert project audit

13 Jan 2026Geometry, Distances

Erdős Problem #659

Problem statement

Can

n

planar points determine only

O(n/\sqrt{\log n})

distances while every four-point subset determines at least three distinct distances?

The problem was proved after remaining open for 29 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Gemini 3 is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 21 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: Gemini 3
Verification: Lean checked
Open for: 29 years
Research activity: 2/5

9 Apr 2026Geometry

Erdős Problem #960

Problem statement

For planar point sets with no

k

collinear points, how many ordinary lines force an

r

-point subset whose every connecting line is ordinary? Is the threshold

o(n^2)

, or even

O(n)

The problem was disproved after remaining open for 42 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

OpenAI internal model is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 1 problem-page discussion comment were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Conjecture disproved

System: OpenAI internal model
Verification: Erdős Problems site confirmed
Open for: 42 years
Research activity: 1/5

1 Feb 2026Geometry, Distances

Erdős Problem #1089

Problem statement

Let

g_d(n)

be the fewest points in

\mathbb R^d

that always determine at least

n

distances. Estimate

g_d(n)

; in particular, does

g_d(n)/d^{n-1}

have a limit as

d\to\infty

The problem was resolved after remaining open for 51 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Aletheia is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: Aletheia
Verification: Erdős Problems site confirmed
Open for: 51 years
Research activity: 1/5

Number theory

21 May 2026Integer sequences and formal proof

Forty-four OEIS conjectures

Problem statement

How many research-level conjectures from the OEIS benchmark can a proof-search agent solve with complete, kernel-checkable Lean proofs?

A formal proof-search system produced Lean-checked proofs for 44 of 492 conjectures drawn from the Online Encyclopedia of Integer Sequences. The same evaluation also solved nine of 353 open Erdős problems.

Details and sources

AI contribution

The agent searched for proofs against fixed formal statements; Lean's kernel checked the resulting proof terms.

Verification

Lean checked

Publication

Public research paper with formal proof artifacts

Activity evidence

The benchmark spans hundreds of discrete conjectures and provides a broad test of formal mathematical reasoning rather than a single research thread.

This portfolio entry summarizes the OEIS portion of the benchmark. Individually documented Erdős results remain separate records in the index.

Research paper

44 conjectures proved

System: Google DeepMind formal proof-search agent
Verification: Lean checked
Research activity: 4/5

1 Jun 2026Multiplicative number theory

Divisibility set for a generalized Euler totient

Problem statement

Define

\varphi_k(n)=\sum_{1\leq a\leq n,(a,n)=1}a^k

and

\mathcal D_s=\{k\geq s:\varphi_s(n)\mid\varphi_k(n)\text{ for every }n\}

. Is

\mathcal D_1=\{1,3,15\}

Campbell proves the exact classification $\mathcal D_1=\{1,3,15\}$ conjectured by Büyükaşik and collaborators in 2024.

Details and sources

AI contribution

The author says the proof is based on extensive interactions with GPT-5.5 Pro.

Verification

Author-checked preprint

Publication

Complete arXiv proof submitted for publication

Activity evidence

A concrete 2024 conjecture supported by computation, but with a short and specialist literature trail.

This is a young but precise published conjecture, included separately from long-running legacy problems.

Research paper

Conjecture proved

System: GPT-5.5 Pro
Verification: Author-checked preprint
Open for: 2 years
Research activity: 2/5

21 May 2026Extremal number theory

Erdős Problem #12 — divisor-avoiding sets

Problem statement

Let

A\subset\mathbb N

be infinite with no distinct

a,b,c\in A

such that

a\mid(b+c)

and

b,c>a

. Can

|A\cap[1,N]|/\sqrt N

have positive lower limit? Must every such

A

fall below

N^{1-c}

infinitely often for some absolute

c>0

AlphaProof Nexus constructs a set of size at least $N/(\log N)^{O(\!\log\log\log N\!)}$ up to $N$ while avoiding the forbidden divisibility pattern. This answers part (i) positively and disproves part (ii); the reciprocal-sum part remains open.

Details and sources

AI contribution

The system autonomously developed a block-and-CRT construction using progression-free sets and produced its Lean proof.

Verification

Lean checked

Publication

AP Nexus preprint, natural-language proof, and Lean source

Activity evidence

A decades-old Erdős problem with several substantial specialist partial results by Schoen, Baier, and Elsholtz–Planitzer.

The parent record has three clauses. The site therefore keeps this as partial even though the first two clauses receive definitive answers.

Official problem record AP Nexus paper Lean artifacts

Two of three parts resolved

System: AlphaProof Nexus
Verification: Lean checked
Open for: 56 years
Research activity: 4/5

4 Feb 2026Bernoulli numbers and class groups

Almost all primes are partially regular

Problem statement

For how large an initial range of even indices

2k

can one prove that almost every odd prime

p

does not divide the numerator of

B_{2k}

, and hence that the corresponding even class-group eigenspaces vanish?

For every $\alpha>1/2$ , a density-one set of odd primes $p$ avoids divisibility by $p$ in all relevant Bernoulli numerators up to $\sqrt p/(\log p)^\alpha$ , yielding corresponding initial class-group vanishing by reflection.

Details and sources

AI contribution

AxiomProver autonomously converted the natural-language argument into a complete Lean development; humans wrote and checked the exposition.

Verification

Published and Lean checked

Publication

Archiv der Mathematik (2026), with public Lean package

Activity evidence

The exact density-one bound is new, while irregular primes, Bernoulli numerators, and Vandiver’s conjecture form a long-running international program.

This is a new partial regularity theorem. It does not solve the Kummer–Vandiver conjecture.

Research paper Published article Lean source

Density-one range proved

System: AxiomProver
Verification: Published and Lean checked
Open for: New theorem inside a 100+ year program
Research activity: 4/5

31 Mar 2026Modular forms

Ramanujan’s tau function misses almost all primes

Problem statement

Let

S(X)=\#\{\ell\leq X:\ell\text{ prime and }|\tau(n)|=\ell\text{ for some }n\}

. Does abc imply

S(X)=o(\pi(X))

Assuming the abc conjecture, the primes occurring as absolute values $|\tau(n)|$ have density zero among all primes.

Details and sources

AI contribution

AxiomProver autonomously proved and formalized the main counting engine and conditional theorem using the stated abc hypothesis and a cited prior proposition.

Verification

Published and Lean checked

Publication

Indagationes Mathematicae article and public Lean source

Activity evidence

Values omitted by Ramanujan’s tau function and related Diophantine questions form a substantial, long-running modular-forms program.

The theorem is conditional on abc. It neither proves Lehmer’s nonvanishing conjecture nor settles whether $\tau$ takes infinitely many prime values.

Research paper Published article Lean source

Conditional density theorem

System: AxiomProver
Verification: Published and Lean checked
Open for: New conditional theorem in a classical program
Research activity: 4/5

18 Jun 2026Prime factors in intervals

Erdős Problem #451 — blocks avoiding middle-sized prime factors

Problem statement

Let

n_k

be the least integer greater than

2k

for which

\prod_{i=1}^{k}(n_k-i)

has no prime factor in

(k,2k)

. How rapidly must

n_k

grow?

The conjectured superpolynomial growth is established: for all sufficiently large $k$ , $n_k>\exp(\!\log^2k/(20\log\log k)\!)$ . Determining the sharper order of $n_k$ remains open.

Details and sources

AI contribution

GPT-5.5 Pro and Quanyu Tang generated the argument; Tang and Wouter van Doorn then wrote and checked the human paper.

Verification

Human-checked arXiv proof

Publication

Public arXiv preprint and official problem-page update

Activity evidence

A 1979 specialist conjecture with classical bounds, a focused modern discussion, and a dedicated 2026 paper.

The growth conjecture is proved, but the original problem also asks for an estimate of $n_k$ , so the entry remains partial.

Official problem record Research paper Research discussion

Superpolynomial growth proved

System: GPT-5.5 Pro
Verification: Human-checked arXiv proof
Open for: 47 years
Research activity: 3/5

10 Jun 2026Multiplicative combinatorics

Erdős Problem #539 — growth of cofactor sets

Problem statement

For

|A|=n

, how small can

Q(A)=\{a/\gcd(a,b):a,b\in A\}

be? Equivalently, estimate

h(n)=\min_{|A|=n}|Q(A)|

ProofCouncil proves $h(n)\leq n^{1/2}\exp(O(\sqrt{\log n}))$ . With the classical lower bound this determines $h(n)=n^{1/2+o(1)}$ , while sharper subpolynomial factors remain open.

Details and sources

AI contribution

A GPT-5.5-Pro-driven author–critic council developed and stress-tested the proof through multiple specialized agents.

Verification

Official update + Lean record

Publication

Public agent paper, code, and official problem-page update

Activity evidence

A sustained specialist line involving Erdős–Szemerédi, Freiman–Lev, Granville–Roesler, and a new multi-author agent paper.

The exponent is settled, which is the principal asymptotic milestone, but the exact subpolynomial behavior is not.

Official problem record ProofCouncil paper Public agent code

Main exponent determined

System: ProofCouncil / GPT-5.5 Pro
Verification: Official update + Lean record
Open for: 53 years
Research activity: 3/5

19 Jun 2026Unit fractions

Erdős Problem #306 — reciprocal semiprimes

Problem statement

a/b\in\mathbb Q_{>0}

and

b

is squarefree, can

a/b

always be written as a finite sum of reciprocals

1/n_i

where the

n_i

are distinct products of two distinct primes?

A public Lean development gives an affirmative proof for every positive rational with squarefree denominator, subject to two explicitly isolated Rosser–Schoenfeld analytic inputs. The official problem page still lists the problem as open.

Details and sources

AI contribution

The repository discloses AI assistance but does not name the model; a separate earlier Claude-assisted result addressed only a partial case.

Verification

Lean checked modulo two named inputs

Publication

Public repository and archived formal artifact

Activity evidence

An established unit-fraction problem with historical constructions, a substantive forum thread, and a reproducible formal artifact.

This is deliberately not labeled a confirmed full resolution until the analytic inputs are fully discharged and the official record or a human manuscript accepts the proof.

Official problem record Lean repository Archived artifact

Candidate full proof

System: AI-assisted Lean development
Verification: Lean checked modulo two named inputs
Open for: 46 years
Research activity: 3/5

14 Jun 2026Distribution of powerful numbers

Erdős Problem #942 — powerful numbers between squares

Problem statement

Let

h(n)

count powerful integers

m\in[n^2,(n+1)^2)

, where

p\mid m

implies

p^2\mid m

. What is the extremal order of

h(n)

Infinitely often, the number of powerful integers in $[n^2,(n+1)^2)$ is at least a constant times $\log n/(\log\log n\,\log\log\log n)$ , improving the earlier exponent- $1/3$ result.

Details and sources

AI contribution

The author reports assistance from several models in developing and formalizing the fixed-parameter construction.

Verification

Lean checked

Publication

Official problem update with linked paper and Lean source

Activity evidence

A classical 1976 question with published 2004 progress and a substantial modern proof-and-formalization thread.

The extremal order of the counting function remains open, so this is a strong lower-bound advance rather than a resolution.

Official problem record Research discussion and artifacts Paper and Lean repository

Lower bound improved

System: Claude / Codex / Aristotle
Verification: Lean checked
Open for: 50 years
Research activity: 3/5

25 Feb 2026Additive number theory

Odd composites beyond powers of two and primes

Problem statement

Can the odd integers not representable as

2^k+p

, with

p

prime, be written as an infinite arithmetic progression together with a density-zero exceptional set?

A Lean development formalizes the negative answer proved by Chen in 2023.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Antigravity / Gemini 3.1 Pro
Verification: Lean checked

24 Nov 2025Additive bases

Density-zero additive complements

Problem statement

For every infinite

A\subseteq\mathbb N

, is there a density-zero set

B

such that

A+B

contains all sufficiently large integers?

ChatGPT expanded Lorentz's classical argument and Aristotle produced a checked Lean formalization.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: ChatGPT / Aristotle
Verification: Lean checked

27 May 2026Extremal number theory

Pairwise-coprime extremal sets

Problem statement

Let

N\geq p_k

, where

p_k

is the

k

th prime. If

A\subseteq\{1,\ldots,N\}

contains no

k+1

pairwise-coprime elements, is

|A|

at most the number of integers in

[N]

divisible by one of the first

k

primes?

The known negative answer and its counterexample now have an AI-assisted Lean verification.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle / GPT
Verification: Lean checked

4 May 2026Multiplicative number theory

Erdős primitive-set inequality

Problem statement

Among primitive sets of integers greater than one, is the weighted reciprocal sum from Erdős's conjecture maximized by the primes?

The modern affirmative proof now has an AI-assisted Lean formalization.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Codex
Verification: Lean checked

24 Nov 2025Sidon sets

Sidon sets meeting every arithmetic progression

Problem statement

Must the complement of every infinite Sidon set contain an infinite arithmetic progression?

AlphaProof found the explicit Sidon set $\{(n+1)!+n:n\geq0\}$ meeting every infinite arithmetic progression; the construction was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Earlier statement file (contains sorry) Discussion thread Community AI ledger

AI-assisted Lean formalization

System: AlphaProof / Aristotle / GPT
Verification: Lean checked

21 Dec 2025Binomial coefficients

Binomial-coefficient divisibility depth

Problem statement

Let

S(n)

be the largest exponent such that every nontrivial

\binom nk

is divisible by some prime to that exponent. Is

\limsup S(n)=\infty

Seed Prover 1.5 found a new proof of the affirmative result, and a Lean proof artifact is recorded.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Seed Prover 1.5
Verification: Lean checked

27 Dec 2025Elementary number theory

Product-minus-sum representations

Problem statement

Does some fixed

k

let every sufficiently large integer be written as

\prod_{i=1}^k a_i-\sum_{i=1}^k a_i

with all

a_i\geq2

AI systems found and formally checked the short affirmative construction with $k=2$ .

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle / ChatGPT
Verification: Lean checked

15 Mar 2026Covering systems

Divisor covering systems with coprime overlaps

Problem statement

Does there exist

n

and, for every divisor

d\mid n

with

d>1

, a residue class

a_d\pmod d

such that the classes cover every integer and any two intersecting classes have coprime moduli?

Adenwalla's negative solution was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

28 Apr 2026Unit fractions

Greedy Egyptian underapproximations

Problem statement

For almost every real

x

, are its best

n

-term unit-fraction underapproximations eventually produced by the greedy algorithm?

Kovač's theorem that the eventually-greedy set has measure zero was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

31 Jan 2026Additive bases

Sparse additive complements to powers of two

Problem statement

Is there a set

A

with

|A\cap[1,N]|=O(N/\log N)

such that every sufficiently large integer is

2^k+a

for some

a\in A

Ruzsa's affirmative construction, using van Doorn's exposition, was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

4 Apr 2026Additive prime number theory

Unbounded prime-plus-set representations

Problem statement

Let

A\subseteq\mathbb N

satisfy

|A\cap\{1,\ldots,N\}|\gg\log N

for all sufficiently large

N

, and let

f(n)

count representations

n=p+a

. Must

\limsup f(n)=\infty

The stronger Chen–Ding affirmative theorem was formalized in Lean conditional on a named Maynard–Tao input.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked conditional on Maynard–Tao input

Publication

Official problem record, discussion, and public formal-proof source

The Lean file is explicit about its custom Maynard–Tao axiom. It verifies the deduction conditional on that analytic input, not the input itself.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked conditional on Maynard–Tao input

28 Dec 2025Complete sequences

Completeness of mixed-power sequences

Problem statement

For coprime integers

a,b>1

, is every sufficiently large integer a sum of distinct numbers

a^k b^\ell

Birch's affirmative theorem was reconstructed and verified in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

21 Apr 2026Irrationality

Irrational squarefree Möbius series

Problem statement

Is the series

\sum_{n\geq1}\mu(n)^2n/2^n

irrational?

The stronger Chen–Ruzsa infinite-subseries theorem was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

26 May 2026Reciprocal sums

Interior of reciprocal subset-sum triples

Problem statement

Do the three shifted reciprocal sums formed from convergent infinite subsets have a set of values with nonempty interior in

\mathbb R^3

Kovač's affirmative theorem was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

20 Jan 2026Covering systems

Covering consecutive integers by congruences

Problem statement

r

congruence classes cover

2^r

consecutive integers, must those classes cover all integers?

The affirmative theorem of Balister, Bollobás, Morris, Sahasrabudhe, and Tiba was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

18 Apr 2026Covering systems

Sparse covering-congruence obstruction

Problem statement

Let

n_1<n_2<\cdots

and choose classes

a_k\pmod{n_k}

, with

n_k>(1+\epsilon)k\log k

for some

\epsilon>0

and every

k

. Must the number of

m<n_k

uncovered by the first

k

classes fail to be

o(k)

Cambie's powers-of-two construction disproving the proposed obstruction was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

14 Jan 2026Unit fractions

Denominator drops in harmonic intervals

Problem statement

For every starting point

a

, can extending a consecutive reciprocal sum by one term reduce its denominator in lowest terms?

Van Doorn's affirmative construction with a linear bound was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

26 May 2026Unit fractions

Disjoint unit-fraction decompositions

Problem statement

How many pairwise-disjoint subsets of

[N]

can each have reciprocal sum one?

The asymptotic value $(1-o(1))\log N$ was formalized from the Hunter–Sawhney observation and Bloom's theorem.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

21 Dec 2025Ramsey theory for unit fractions

Monochromatic unit-fraction equations

Problem statement

Does every finite coloring of the positive integers contain distinct monochromatic

a,b,c

satisfying

1/a=1/b+1/c

The Brown–Rödl affirmative theorem received a public Lean proof.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Earlier statement file (contains sorry) Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Seed Prover 1.5
Verification: Lean checked

1 Apr 2026Unit fractions

Near-unit harmonic intervals

Problem statement

For the first consecutive harmonic block beginning at

n

whose sum reaches one, is the scaled overshoot characterized by

\liminf n^2\epsilon(n)=0

The Lim–Steinerberger affirmative theorem was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

31 Jan 2026Unit fractions

Vardi-constant extremality

Problem statement

Does every non-Sylvester reciprocal decomposition of one have a smaller doubly-exponential growth constant than the Vardi constant?

Kamio's affirmative extremal theorem was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

10 Dec 2025Additive bases

Sparse additive-basis doubling

Problem statement

For every zero-density additive basis

A

, must

|(A+A)\cap[1,N]|/|A\cap[1,N]|

tend to infinity?

The Ruzsa–Turjányi counterexample was formalized in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Aristotle
Verification: Lean checked

25 Nov 2025Additive combinatorics

Reciprocal sums of dissociated sets

Problem statement

If every subset sum of a finite set

A\subset\mathbb N

is distinct, must

\sum_{n\in A}1/n<2

ChatGPT supplied a proof explanation of Ryavec's affirmative theorem and Aristotle formalized it in Lean.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: ChatGPT / Aristotle
Verification: Lean checked

29 May 2026Additive number theory

Extremal Frobenius-number asymptotics

Problem statement

For coprime

k

-element sets

A\subseteq\{1,\ldots,n\}

, is the maximum Frobenius number asymptotic to

n^2/(k-1)

Dixmier's affirmative theorem was formalized in an unconditional Lean development using a mixed open-harness and proprietary-model workflow.

Details and sources

AI contribution

AI systems contributed proof search, proof reconstruction, or formal proof engineering; Lean's kernel checked the resulting artifact.

Verification

Lean checked

Publication

Official problem record, discussion, and public formal-proof source

This record distinguishes an AI-produced proof or formalization from mathematical priority: the underlying result may have been known before the AI work.

Problem, history, and proof record Formal proof source Discussion thread Community AI ledger

AI-assisted Lean formalization

System: Gemini 3.1 Pro / Gemini 3.0 Flash / Claude Sonnet 4.6 / Project Numina / Aristotle / Claude Opus 4.8 / ulam.ai CLI harness
Verification: Lean checked

4 May 2026Multiplicative number theory

Erdős Problem #456 — totient preimages and least primes

Problem statement

Let

p_n

be the least prime congruent to

1\pmod n

and

m_n

the least integer with

n\mid\varphi(m_n)

. Is

m_n<p_n

almost always, does

p_n/m_n\to\infty

almost always, and when is

m_n=p

unique?

A 71-page discussion manuscript claims unconditional negative answers to the first two questions and a Dickson-conditional answer to the third.

Details and sources

AI contribution

The author reports using an automated multi-turn GPT-5.5 Pro scaffold to develop and repeatedly audit the argument.

Verification

Community manuscript; expert review requested

Claim audit

The official problem page still marks the problem open, and the author explicitly requests expert review or formalization.

Publication

Public discussion thread and linked manuscript

Activity evidence

A multi-part 1979 Erdős problem with classical input from Linnik-type prime bounds and an active recent discussion.

The first two conclusions are claimed unconditional; the third depends on Dickson's conjecture. This record documents the claim without promoting it to a confirmed resolution.

Official problem record Claim, manuscript, and discussion

Mixed solution claimed

System: GPT-5.5 Pro audit-and-revise scaffold
Verification: Community manuscript; expert review requested
Claim audit: Issue documented
Open for: 47 years
Research activity: 3/5

27 Apr 2026Sieve theory and gaps in sifted sets

Erdős Problem #1101 — subexponential good sequences

Problem statement

Does there exist a good pairwise-coprime sequence

u_n

with

\sum 1/u_n<\infty

and polynomial growth? What if one only requires

u_n\leq e^{o(n)}

A community note reports a subexponential good-sequence construction with help from GPT-5.5 Pro. The full polynomial-growth question remains open.

Details and sources

AI contribution

The contributor credits GPT-5.5 Pro with assisting the partial-result argument.

Verification

Community partial result

Publication

Official problem record, discussion, and linked note

Activity evidence

A specialist 1981 Erdős problem linking sieve gaps and structured sequences, with a small but substantive recent discussion.

The official page explicitly classifies the discussion as partial and continues to mark both main questions open.

Official problem and partial-result status Discussion and linked note

Partial construction claimed

System: GPT-5.5 Pro
Verification: Community partial result
Open for: 45 years
Research activity: 2/5

7 May 2026Covering systems

Erdős Problem #7 — failed odd-covering-system formalization

Problem statement

Can there be a finite covering system of the integers with distinct moduli, all of which are odd and greater than

1

A claimed proof that no distinct covering system can have only odd moduli does not establish the conjecture. Its central Lean axiom states that a product of factors greater than one is less than one.

Details and sources

AI contribution

The author used Lean and an Aristotle audit to check the monotonicity layer, while leaving three purported consequences of the BBMST sieve as axioms. GPT-assisted community review helped identify the fatal mismatch.

Verification

Failed axiom and statement-fidelity audit

Claim audit

The encoded sieve product omitted the BBMST initial LP factor $c_0\approx0.098$ . Under the submitted definition every update factor is greater than $1$ , so the axiom `bbmst_sf_lt_one` is impossible. The author acknowledged the mistranslation.

Publication

Public manuscript, Lean repository, archived release, and corrective discussion

Activity evidence

A longstanding prize problem with major sieve-theoretic progress and an unusually detailed public audit of an AI-assisted formal claim.

The underlying Erdős–Selfridge odd covering-system problem remains open. A sorry-free derivation from a false imported axiom is not an end-to-end formal proof.

Official problem record Discussion, objection, and correction Submitted manuscript and Lean code Archived release

Claim withdrawn after a false axiom was found

System: Aristotle audit + GPT-assisted discussion
Verification: Failed axiom and statement-fidelity audit
Claim audit: Issue documented
Open for: Still open after the failed claim
Research activity: 5/5

24 Jun 2026Analytic number theory

Erdős Problem #1061 — divisor-sum solution growth

Problem statement

For

S(x)=\#\{(a,b)\in\mathbb N^2:a+b\leq x,\ \sigma(a)+\sigma(b)=\sigma(a+b)\}

, is

S(x)\sim cx

for some

c>0

A preprint claims that the number $S(x)$ of ordered pairs with $a+b\leq x$ and $\sigma(a)+\sigma(b)=\sigma(a+b)$ grows faster than $x(\log x)^R$ for every fixed $R>0$ , ruling out the proposed linear asymptotic.

Details and sources

AI contribution

The author reports extensive ChatGPT use for technical lemmas, calculations, code, proof development, and auditing while retaining the strategic direction and final responsibility.

Verification

Public self-contained preprint; independent review pending

Publication

Public arXiv proof and official discussion record

Activity evidence

The question appears in Guy’s collection and intersects active work on divisor sums, prime patterns, and additive equations.

The manuscript is a substantive claimed resolution, but the official problem record still treats it as open while the proof is reviewed. This entry therefore does not imply community acceptance.

Claimed proof Official problem record Discussion thread

Claimed resolution under expert review

System: ChatGPT
Verification: Public self-contained preprint; independent review pending
Open for: Official record still open
Research activity: 4/5

27 Jun 2026Probabilistic number theory

Erdős Problem #731 under dyadic regularity

Problem statement

A(n)

is the least positive integer not dividing

\binom{2n}{n}

, is there a reasonable function

f(n)

such that

A(n)\sim f(n)

for almost all

n

For the least positive integer $A(n)$ not dividing $\binom{2n}{n}$ , a preprint proves a density-tight logarithmic scale and rules out an asymptotic equivalent for every dyadically regular deterministic normalization.

Details and sources

AI contribution

The author reports extensive ChatGPT use for proof exploration, technical lemmas, calculations, code, and auditing.

Verification

Public proof; no independent review or formal certificate located

Claim audit

Scope is deliberately narrower than the literal informal question: the no-asymptotic-equivalent theorem assumes dyadic regularity, and sharper limiting-distribution questions remain open.

Publication

Public arXiv proof and official problem discussion

Activity evidence

The least-nondivisor problem has a long history involving Kummer carries, missing primes, and almost-all asymptotics.

The word “reasonable” in the original problem is informal. This paper gives and resolves an explicit broad block-smooth interpretation; it does not exclude every possible irregular deterministic scale.

Variant proof and exact scope Official problem record Discussion thread

Explicit regularity variant claimed

System: ChatGPT
Verification: Public proof; no independent review or formal certificate located
Claim audit: Issue documented
Open for: Variant of an open-ended Erdős problem
Research activity: 4/5

12 Jun 2026Experimental number theory

Sun Conjecture 4.6(ii) on trigonometric permanents

Problem statement

For an odd prime

p

, do Sun’s normalized trigonometric permanents satisfy

s_p<0\iff p\equiv5\pmod{12}

and

s'_p<0\iff p\equiv7\pmod8

Exact calculations at $p=29$ refute both proposed sign laws: $s_{29}>0$ despite $29\equiv5\pmod{12}$ , while $s'_{29}<0$ despite $29\not\equiv7\pmod8$ .

Details and sources

AI contribution

The pipeline generated counterexamples and four algorithmically independent exact layers using cyclotomic arithmetic, finite fields, CRT uniqueness, and subset dynamic programming.

Verification

Multiple independent exact implementations; not externally refereed

Publication

Public note, certificates, programs, and frozen source

Activity evidence

A precise computational number-theory conjecture whose published table stopped at the prime immediately before the first failure.

Part (i), the divisibility assertion for odd composite $n$ , was not refuted and remains open. No replacement sign law is claimed.

Original conjecture Result page and exact scope Certificates and independent implementations Verification catalog and runnable checks

Both sign clauses in part (ii) refuted

System: Demonstrandum multi-agent pipeline
Verification: Multiple independent exact implementations; not externally refereed
Open for: Unchanged since the 2021 conjecture
Research activity: 2/5

22 May 2026Digital number theory

Binary digits of the Erdős–Borwein constant

Problem statement

For the Erdős–Borwein constant

E=\sum_{n\geq1}\frac{1}{2^n-1},

does the block

11

occur infinitely often in the base-2 expansion of

E

John M. Campbell proved that the block 11 occurs infinitely often in the binary expansion of the Erdős–Borwein constant, using a congruence construction and a prime-counting estimate.

Details and sources

AI contribution

The author reports that the argument was developed through extensive interactions with GPT-5.5 Pro.

Verification

Author-checked preprint

Publication

Complete arXiv proof submitted for publication

Activity evidence

A recognized 2012 question of Crandall, later repeated by Shallit, with a limited rather than large sustained literature.

The paper gives a conventional complete proof and credits extensive AI interaction, but does not separate which individual lemmas originated with the model.

Research paper

Open problem proved

System: GPT-5.5 Pro
Verification: Author-checked preprint
Open for: 14 years
Research activity: 2/5

Jun 2026Additive number theory

Erdős Problem #477 — polynomial tiling complements

Problem statement

Does there exist an integer polynomial

f

of degree at least two and a set

A\subseteq\mathbb{Z}

such that every integer has a unique representation

n=a+f(k),\qquad a\in A,\ k\in\mathbb{Z}?

A June 2026 manuscript claims that the thirteenth powers have a tiling complement in the integers, which would answer the existence question positively.

Details and sources

AI contribution

The pipeline repository says GPT-5.5 Pro generated the proof and that human contributors polished and verified the resulting manuscript.

Verification

Author-checked manuscript; official record open

Publication

Public proof manuscript and open pipeline

Activity evidence

A substantial but narrow additive-tiling question recorded by Erdős and Graham in 1980, with limited documented follow-up.

The candidate is existential and constructive, using $f(m)=m^{13}$ . The official Erdős Problems record still listed #477 as open when checked on 25 July 2026.

Proof manuscript Official problem record Solver–verifier pipeline

Candidate construction

System: GPT-5.5 Pro
Verification: Author-checked manuscript; official record open
Open for: 46 years
Research activity: 2/5

6 Jul 2026Algebraic number theory

The $2$ -adic absolute Galois group

Problem statement

Give an explicit profinite presentation of the absolute Galois group

\operatorname{Gal}(\overline{\mathbb{Q}}_2/\mathbb{Q}_2)

Claude Fable 5 and, independently, GPT-5.5 Pro produced presentations accepted by FrontierMath’s bespoke verifier. The contributor regards them as likely correct, but a full proof is still being reconstructed and checked.

Details and sources

AI contribution

Two separate systems generated candidate profinite presentations that passed the problem-specific computational verifier.

Verification

Verifier accepted; proof pending

Publication

Epoch AI progress update; no complete proof manuscript yet

Activity evidence

A solid specialist problem in local Galois theory. Epoch rates a full solution as a solid result, but reports a relatively small specialist community.

This remains a partial result. Passing the verifier is strong evidence that the proposed presentations have the required finite-quotient behavior, but Epoch explicitly says it is short of a proof.

Problem and progress update

Verifier-accepted presentation; proof pending

System: Claude Fable 5 / GPT-5.5 Pro
Verification: Verifier accepted; proof pending
Open for: Longstanding; date unclear
Research activity: 3/5

5 Mar 2026Diophantine equations

Two small Diophantine equations

Problem statement

Prove that each of the nine listed small Diophantine equations has infinitely many integer solutions. GPT-5.4 Pro resolved

z^2+y^2z-z+x^3+2=0

and

z^2+y^2z+x^3+x+1=0

by finding three distinct solutions with

|x|>10^{50}

and then giving parametric families.

GPT-5.4 Pro found direct substitutions giving infinitely many integer solutions for two equations in a nine-equation FrontierMath portfolio. The authors adapted one substitution to a third equation; six remain open.

Details and sources

AI contribution

The model produced two explicit parametric families satisfying the large-solution requirement.

Verification

Problem authors checked

Publication

Epoch AI write-up and public six-page solution note

Activity evidence

Epoch reports 2–4 mathematicians familiar with and seriously attempting the portfolio, and rates a full solution as moderately interesting.

The parent challenge is not solved. This record is deliberately classified as partial because the benchmark requires all nine equations to be resolved.

Problem and status Two AI-found families

Two of nine equations solved

System: GPT-5.4 Pro
Verification: Problem authors checked
Open for: Date not fixed
Research activity: 2/5

13 Apr 2026Number theory

Erdős Problem #1196

Problem statement

A\subseteq[x,\infty)

is primitive—no member divides another—must

\sum_{a\in A}1/(a\log a)\leq1+o(1)

x\to\infty

A von Mangoldt Markov-chain method proves the primitive-set bound and settles several related conjectures, including Erdős Problems #1217 and #164.

Details and sources

AI contribution

Liam Price launched the autonomous query; a human team including Terence Tao then checked, developed, and generalized the method.

Verification

Multi-author human proof

Publication

Detailed arXiv preprint and public expert exposition

Activity evidence

A 1966 conjecture with several published partial bounds and a dedicated multi-author resolution.

This is a particularly transparent case: the initial model conversation, the human mathematical development, and the resulting preprint can be compared directly. No formal proof assistant artifact was located.

Original ChatGPT conversation Tao’s exposition Preprint Official problem record

Resolved and extended

System: GPT-5.4 Pro
Verification: Multi-author human proof
Open for: 60 years
Research activity: 4/5

6 Jan 2026Number theory

Erdős Problem #728

Problem statement

For fixed

C>0

and sufficiently small

\epsilon>0

, are there infinitely many

a,b,n

with

a,b\geq\epsilon n

a!b!\mid n!(a+b-n)!

, and

a+b>n+C\log n

A logarithmic-gap theorem for a factorial divisibility problem resolves the agreed formulation and also gives solutions to Problems #729 and #401.

Details and sources

AI contribution

GPT-5.2 supplied the informal argument and Harmonic’s Aristotle produced a kernel-checked Lean proof.

Verification

Lean checked + human writeup

Publication

Lean source and a detailed arXiv translation are public

Activity evidence

One original source, extensive later discussion, and a dedicated human writeup.

The first generated proof addressed an ambiguous weaker reading. A second autonomous run handled the formulation accepted by the forum, after which the result gained community consensus.

Human-readable proof Lean proof Public writeup chat

Fully resolved

System: GPT-5.2 Pro + Aristotle
Verification: Lean checked + human writeup
Open for: 51 years
Research activity: 3/5

25 Nov 2025Extremal number theory

Erdős Problem #56 — missing-hypothesis audit

Problem statement

For

N\geq p_k

, if

A\subseteq\{1,\ldots,N\}

contains no

k+1

pairwise relatively prime elements, is

A

no larger than the set of multiples of the first

k

primes?

Aristotle found a Lean-checked counterexample to the first formal statement at $N=k=2$ . The counterexample exposed a missing hypothesis, $N\geq p_k$ , rather than disproving the intended Erdős problem.

Details and sources

AI contribution

Aristotle independently falsified the faulty encoded statement. After the missing condition was identified, ChatGPT explained the literature proof and Aristotle formalized the corrected theorem.

Verification

Lean checked; target statement was faulty

Claim audit

Missing hypothesis: the initial formal statement omitted $N\geq p_k$ , making it trivially false.

Publication

Official Erdős discussion, corrected problem statement, and repaired Lean formalization

This is not a failure of Lean’s kernel. Lean correctly certified a counterexample to the proposition it was given; the failure was the mismatch between that proposition and the intended mathematical claim.

Official problem and discussion Revision history Formalization post-mortem

Formal statement repaired

System: Aristotle + ChatGPT
Verification: Lean checked; target statement was faulty
Claim audit: Issue documented

28 Nov 2025Diophantine approximation

Erdős Problem #480 — variable-mismatch audit

Problem statement

For every sequence

x_1,x_2,\ldots\in[0,1]

, must

\inf_{n\geq1}\liminf_{m\to\infty}n\lvert x_{m+n}-x_m\rvert\leq5^{-1/2}\,?

Aristotle automatically proved an encoded statement that was not the intended theorem: the Lean hypothesis said $m\ne0$ where it should have said $n\ne0$ . The proof also exploited Lean’s totalized division convention, where $1/0=0$ .

Details and sources

AI contribution

The prover completed the supplied Lean goal, revealing that the goal itself admitted an unintended route.

Verification

Lean checked; wrong variable in target

Claim audit

Low-level specification bug: $m\ne0$ replaced the intended condition $n\ne0$ , enabling a proof of the wrong proposition.

Publication

Official Erdős discussion, public Lean proof, and filed correction issue

The mathematical theorem was already known from Chung and Graham. This case is retained because it cleanly separates kernel correctness from correctness of the formal specification.

Official problem and audit discussion Formalization post-mortem

Misformalization detected

System: Aristotle
Verification: Lean checked; wrong variable in target
Claim audit: Issue documented

27 Nov 2025Multiplicative number theory

Erdős Problem #488 — corrected-target audit

Problem statement

For a finite set

A

, let

B

be the positive integers divisible by some

a\in A

. For every

m>n\geq\max(A)

, must

\frac{\lvert B\cap[1,m]\rvert}{m}<2\frac{\lvert B\cap[1,n]\rvert}{n}\,?

Aristotle found and Lean-checked a finite counterexample to the statement then encoded in Formal Conjectures. Source comparison showed that this was likely a misstated “non-divisibility” version; the corrected “divisibility” problem remains open.

Details and sources

AI contribution

Given only the formal statement, Aristotle produced the counterexample $n=13$ , $m=200$ , and $A=\{2,3,5,7,11,13\}$ .

Verification

Lean checked; source wording corrected

Claim audit

Source mismatch: the encoded version followed wording now treated as a likely typo in one Erdős source.

Publication

Official problem history, community discussion, and formal counterexample

The certificate is valid for the encoded proposition. It does not settle the corrected version now displayed by the Erdős database.

Current problem record Counterexample and correction discussion Problem revision history Formalization post-mortem

Counterexample to obsolete wording

System: Aristotle
Verification: Lean checked; source wording corrected
Claim audit: Issue documented

23 Apr 2026Covering systems

Erdős Problem #202

Problem statement

Let

n_1<\cdots<n_r\leq N

and choose pairwise-disjoint residue classes

a_i\pmod{n_i}

. How large can

r

be as a function of

N

The conjectured asymptotic statement for a covering-system problem was proved by GPT-5.4 Pro under human prompting and checking.

Details and sources

AI contribution

Boon Suan Ho prompted the model, checked the output, and presented the result to the Erdős Problems community.

Verification

Community checked + formal artifact reported

Publication

Public problem discussion and community record

Activity evidence

7 cited source records and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The entry records the accepted problem-site status. It does not treat the absence of a conventional journal article as evidence against the proof.

Problem record Discussion thread Community AI ledger

Conjectured asymptotic proved

System: GPT-5.4 Pro
Verification: Community checked + formal artifact reported
Open for: 65 years
Research activity: 4/5

4 Feb 2026Complete sequences

Erdős Problem #347

Problem statement

Is there an integer sequence with

a_{n+1}/a_n\to2

whose finite subset sums have density 1 even after deleting any finite number of terms?

A problem of Erdős and Graham on complete sequences was resolved through a multi-person, multi-system collaboration.

Details and sources

AI contribution

AI systems proposed and formalized components while human collaborators reconciled the statement, proof structure, and historical sources.

Verification

Lean checked

Publication

Public problem record and formal proof artifacts

Activity evidence

1 cited source record and 15 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The result is a full solution, but it is not an autonomous single-model discovery; the provenance is inherently collaborative.

Problem record Community AI ledger

Fully resolved

System: Aristotle + Claude + Codex + GPT
Verification: Lean checked
Open for: 46 years
Research activity: 2/5

7 Mar 2026Number theory

Erdős Problem #650

Problem statement

Given an arbitrary

m

-element set

A\subseteq[1,N]

, how many integers can every interval of length

2N

contain so that each is divisible by a distinct element of

A

? In particular, is the extremal quantity

O(\sqrt m)

The exact value of the matching function f(m) was determined as min(m, ⌈2√m⌉), resolving an Erdős problem on matching integers to distinct multiples.

Details and sources

AI contribution

ChatGPT proposed the proof strategy, AlphaEvolve supported numerical optimization, and Aristotle produced the formal certificate.

Verification

Lean checked + human paper

Claim audit

The first GPT lower-bound proof had a genuine gap: after deleting the midpoint, it still assumed that the next multiple lies in the positive half. Standard human and model checks missed this. Aristotle nevertheless completed the formalization by finding and encoding a repair independently; the final theorem remains valid.

Publication

Public arXiv preprint

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The final exposition is human written and states an optimal theorem stronger and cleaner than the original problem formulation. The Lean proof is valid, but its route is not identical to the initially circulated informal proof.

Preprint Problem record Lean proof Discussion and proof-gap timeline Community AI ledger

Optimal formula proved

System: GPT-5.4 Pro + Aristotle + AlphaEvolve
Verification: Lean checked + human paper
Claim audit: Issue documented
Open for: 31 years
Research activity: 1/5

5 Jun 2026Divisor theory

Erdős Problem #696

Problem statement

Compare the longest prime chain

p_{i+1}\equiv1\pmod{p_i}

inside the divisors of

n

with the analogous longest chain of arbitrary divisors. Does their length ratio tend to infinity for almost every

n

A forty-seven-year-old divisor problem was resolved in a collaborative workflow ending in a kernel-checked Lean proof.

Details and sources

AI contribution

Several models contributed proof ideas and proof engineering while human collaborators coordinated statement fidelity.

Verification

Lean checked

Publication

Public problem record and formal development

Activity evidence

1 cited source record and 1 problem-page discussion comment were located. The score is a conservative proxy for documented research attention.

This is a full mathematical resolution, but the evidence supports a distributed collaboration rather than a single autonomous run.

Problem record Independent tracker entry Community AI ledger

Fully resolved

System: Aristotle + Claude Code + Claude Opus 4.7 + GPT-5.5 Pro
Verification: Lean checked
Open for: 47 years
Research activity: 1/5

29 Jan 2026Irrationality

Erdős Problem #1051

Problem statement

a_1<a_2<\cdots

and

\liminf a_n^{1/2^n}>1

, must

\sum_{n\geq1}1/(a_na_{n+1})

be irrational?

An irrationality problem of Erdős and Graham was solved by Aletheia and certified in Lean.

Details and sources

AI contribution

The generator–verifier–reviser agent produced the argument and a formal system checked the final theorem.

Verification

Lean checked

Publication

Public problem record and autonomous-math evaluation

Activity evidence

2 cited source records and 6 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The result is one of the clearest autonomous Aletheia research cases, although the public record is a paper-level interaction report rather than a raw chat export.

Problem record Aletheia research report Community AI ledger

Problem proved and formalized

System: Aletheia
Verification: Lean checked
Open for: 46 years
Research activity: 2/5

Sep 2025Analytic number theory

Strong Prime Number Theorem

The strong Prime Number Theorem and substantial supporting complex-analysis infrastructure were formalized in Lean.

Details and sources

AI contribution

Gauss generated most statements and proofs from a human-prepared blueprint, with targeted scaffolding and review of key lemmas.

Verification

Lean checked

Publication

Public blueprint, documentation, and Lean repository

This did not discover the Prime Number Theorem. It is classified separately because the contribution is large-scale verification of established mathematics.

Formalization portal Lean repository

Known theorem autoformalized

System: Gauss
Verification: Lean checked

6 Apr 2026Number Theory, Divisors

Erdős Problem #26

Problem statement

Let

A\subset\mathbb{N}

be infinite. Must there exist some

k\geq 1

such that almost all integers have a divisor of the form

a+k

for some

a\in A

Davenport and Erdős had already given a negative answer to the literal problem in 1951. A DeepMind prover agent later found and Lean-verified a stronger counterexample to a variant.

Details and sources

AI contribution

DeepMind prover agent is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 6 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This is an AI contribution to a stronger variant, not the first historical resolution of the literal problem.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Stronger variant disproved

System: DeepMind prover agent
Verification: Lean checked
Open for: Known result; 2026 variant
Research activity: 1/5

25 Apr 2026Number Theory

Erdős Problem #38

Problem statement

Does there exist

B\subset\mathbb{N}

which is not an additive basis, but is such that for every set

A\subseteq\mathbb{N}

of Schnirelmann density

\alpha

and every

N

there exists

b\in B

such that

\lvert (A\cup (A+b))\cap \{1,\ldots,N\}\rvert\geq (\alpha+f(\alpha))N

where

f(\alpha)>0

for

0<\alpha <1

? The Schnirelmann density is defined by

d_s(A) = \inf_{N\geq 1}\frac{\lvert A\cap\{1,\ldots,N\}\rvert}{N}.

The problem was proved after remaining open for 70 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.5 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 1 problem-page discussion comment were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.5 Pro
Verification: Lean checked
Open for: 70 years
Research activity: 1/5

30 Mar 2026Number Theory, Base Representations

Erdős Problem #125

Problem statement

Let

A

be the integers using only digits 0 and 1 in base 3, and

B

the integers using only digits 0 and 1 in base 4. Does

A+B

have positive lower density?

The problem was disproved after remaining open for 30 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

DeepMind prover agent is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

2 cited source records and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Conjecture disproved

System: DeepMind prover agent
Verification: Lean checked
Open for: 30 years
Research activity: 2/5

10 Jan 2026Number Theory

Erdős Problem #205

Problem statement

Must every sufficiently large

n

equal

2^k+m

with

\Omega(m)<\log\log m

? Can the bound be reduced to

\epsilon\log\log m

, or to a still slower-growing function?

The problem was disproved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Aristotle, GPT-5.2 Thinking is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 21 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Conjecture disproved

System: Aristotle, GPT-5.2 Thinking
Verification: Lean checked
Open for: 46 years
Research activity: 2/5

14 Apr 2026Irrationality

Erdős Problem #258

Problem statement

a_1,a_2,\ldots

are positive integers with

a_n\to\infty

, must

\sum_n \tau(n)/(a_1\cdots a_n)

be irrational?

The problem was proved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.4 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

2 cited source records and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.4 Pro
Verification: Lean checked
Open for: 46 years
Research activity: 2/5

3 May 2026Number Theory, Unit Fractions

Erdős Problem #283

Problem statement

Let

p:\mathbb Z\to\mathbb Z

be polynomial with positive leading coefficient and no fixed divisor. Can every sufficiently large

m

be written as

p(n_1)+\cdots+p(n_k)

for

1\leq n_1<\cdots<n_k

with

1/n_1+\cdots+1/n_k=1

The problem was proved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.5 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 2 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.5 Pro
Verification: Lean checked
Open for: 46 years
Research activity: 1/5

24 Apr 2026Number Theory, Additive Basis

Erdős Problem #330

Problem statement

Does there exist a minimal additive basis of positive density such that deleting any one of its members prevents a positive-density set of integers from being represented?

The problem was proved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.5 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 14 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.5 Pro
Verification: Lean checked
Open for: 46 years
Research activity: 2/5

25 Dec 2025Number Theory, Additive Basis

Erdős Problem #333

Problem statement

For every density-zero set

A\subseteq\mathbb N

, does there exist

B

with

A\subseteq B+B

and

|B\cap[1,N]|=o(N^{1/2})

A 1977 theorem of Erdős and Newman already implied the negative answer. The 2025 AI event rediscovered and formalized that conclusion.

Details and sources

AI contribution

Claude Opus 4.5, GPT-5.2 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 14 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The AI contribution is rediscovery and formalization, not mathematical priority.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Known theorem reconstructed

System: Claude Opus 4.5, GPT-5.2 Pro
Verification: Lean checked
Open for: Known by 1977
Research activity: 2/5

3 May 2026Number Theory, Complete Sequences

Erdős Problem #351

Problem statement

For

p(x)\in\mathbb Q[x]

with positive leading coefficient, is the set

\{p(n)+1/n:n\in\mathbb N\}

strongly complete—does every cofinite subcollection have finite subset sums containing all sufficiently large integers?

The problem was proved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.5 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 9 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.5 Pro
Verification: Lean checked
Open for: 46 years
Research activity: 1/5

26 Mar 2026Number Theory

Erdős Problem #369

Problem statement

For every

\epsilon>0

and

k\geq2

, do all sufficiently large intervals

[1,n]

contain

k

consecutive integers that are all

n^\epsilon

-smooth?

The literal database statement is trivial; the AI work addressed an intended stronger variant related to results already present in the literature.

Details and sources

AI contribution

GPT is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This record is classified as a variant because the literal and intended formulations differ.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Intended variant treated

System: GPT
Verification: Lean checked
Open for: Variant record
Research activity: 1/5

31 Mar 2026Number Theory

Erdős Problem #380

Problem statement

Call

[u,v]

bad when the greatest prime factor of

\prod_{u\leq m\leq v}m

occurs with exponent greater than 1. Is the count of integers up to

x

lying in a bad interval asymptotic to the count of

n\leq x

with

P(n)^2\mid n

The problem was proved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.4 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 5 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.4 Pro
Verification: Erdős Problems site confirmed
Open for: 46 years
Research activity: 1/5

10 Jan 2026Number Theory, Binomial Coefficients

Erdős Problem #397

Problem statement

Are there only finitely many identities

\prod_i {2m_i\choose m_i}=\prod_j {2n_j\choose n_j}

when all the

m_i

and

n_j

are distinct?

The negative answer was rediscovered and formalized in 2026; an essentially identical problem had appeared in a 2012 China TST.

Details and sources

AI contribution

Aristotle, GPT-5.2 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 30 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The Lean artifact is a new verification, but the mathematical result was not new in 2026.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Known result rediscovered

System: Aristotle, GPT-5.2 Pro
Verification: Lean checked
Open for: Known by 2012
Research activity: 3/5

11 Jan 2026Number Theory, Factorials

Erdős Problem #401

Problem statement

Can one find a function

f(r)\to\infty

such that infinitely many

n

admit

a_1+a_2>n+f(r)\log n

while

a_1!a_2!

divides

n!2^n3^n\cdots p_r^n

The problem was proved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Aristotle, GPT-5.2 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 18 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: Aristotle, GPT-5.2 Pro
Verification: Lean checked
Open for: 46 years
Research activity: 2/5

2 Mar 2026Number Theory

Erdős Problem #457

Problem statement

Is there

\epsilon>0

such that infinitely many

n

have every prime

p\leq(2+\epsilon)\log n

dividing

\prod_{1\leq i\leq\log n}(n+i)

The problem was proved after remaining open for 47 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Aristotle, GPT-5.2 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

2 cited source records and 1 problem-page discussion comment were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: Aristotle, GPT-5.2 Pro
Verification: Lean checked
Open for: 47 years
Research activity: 2/5

21 Jan 2026Number Theory, Group Theory

Erdős Problem #543

Problem statement

For a finite abelian group

G

of order

N

, let

f(N)

be the smallest size of a random subset that generates every element as a subset sum with probability at least 1/2. Is

f(N)\leq\log_2N+o(\log\log N)

The problem was disproved after remaining open for 53 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.2 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

2 cited source records and 28 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Conjecture disproved

System: GPT-5.2 Pro
Verification: Erdős Problems site confirmed
Open for: 53 years
Research activity: 4/5

8 May 2026Number Theory

Erdős Problem #690

Problem statement

For fixed

k

, is the density

d_k(p)

of integers whose

k

th-smallest prime factor is

p

unimodal as

p

ranges over the primes?

Cambie’s 2025 result had already refuted universal unimodality. The Multiscalar Fields work was a later AI contribution to the resolved problem.

Details and sources

AI contribution

Multiscalar Fields System is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 2 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This record does not attribute the first resolution to the 2026 AI event.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Later AI contribution

System: Multiscalar Fields System
Verification: Erdős Problems site confirmed
Open for: Resolved before AI event
Research activity: 1/5

1 May 2026Number Theory

Erdős Problem #694

Problem statement

f_{\max}(n)

and

f_{\min}(n)

are the largest and smallest solutions of

\phi(m)=n

, how large can

f_{\max}(n)/f_{\min}(n)

be for

n\leq x

The problem was resolved after remaining open for 47 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.5 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 2 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: GPT-5.5 Pro
Verification: Lean checked
Open for: 47 years
Research activity: 1/5

10 Jan 2026Number Theory, Factorials

Erdős Problem #729

Problem statement

For each constant

C>0

, are there infinitely many

a,b,n

with

a+b>n+C\log n

such that the denominator of

n!/(a!b!)

has only bounded prime factors?

The problem was proved after remaining open for 51 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Aristotle, GPT-5.2 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 30 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: Aristotle, GPT-5.2 Pro
Verification: Lean checked
Open for: 51 years
Research activity: 3/5

20 Nov 2025Number Theory

Erdős Problem #848

Problem statement

Is the largest subset

A\subseteq[1,N]

for which

ab+1

is never squarefree attained by the residue class

7\pmod{25}

GPT-5 reduced the question to a finite computation. The official record classifies it as decidable, not as a completed full resolution.

Details and sources

AI contribution

GPT-5 is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 18 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

A finite decision procedure is meaningful progress, but the remaining finite check has not been reported complete.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Resolved up to a finite check

System: GPT-5
Verification: Erdős Problems site confirmed
Open for: 33 years
Research activity: 2/5

5 Feb 2026Number Theory

Erdős Problem #851

Problem statement

For every

\epsilon>0

, is there a bounded

r

such that integers of the form

2^k+n

, with

n

having at most

r

prime factors, have density at least

1-\epsilon

The problem was proved after remaining open for 41 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.2 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.2 Pro
Verification: Erdős Problems site confirmed
Open for: 41 years
Research activity: 1/5

15 Apr 2026Number Theory, Primitive Sets

Erdős Problem #858

Problem statement

How large can

\frac1{\log N}\sum_{n\in A}1/n

be when

A\subseteq[1,N]

contains no relation

at=b

whose multiplier

t

has least prime factor greater than

a

The problem was resolved after remaining open for 56 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.4 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: GPT-5.4 Pro
Verification: Erdős Problems site confirmed
Open for: 56 years
Research activity: 1/5

5 Jan 2026Number Theory, Additive Basis

Erdős Problem #871

Problem statement

A

is an additive basis of order 2 and its representation count tends to infinity, can

A

be partitioned into two disjoint additive bases of order 2?

The problem was disproved after remaining open for 38 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Claude Opus 4.5, Gemini 3 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 13 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Conjecture disproved

System: Claude Opus 4.5, Gemini 3 Pro
Verification: Lean checked
Open for: 38 years
Research activity: 2/5

25 Apr 2026Number Theory, Squares

Erdős Problem #888

Problem statement

How large can

A\subseteq[1,n]

be if every ordered quadruple

a\leq b\leq c\leq d

A

with

abcd

a square must satisfy

ad=bc

The problem was resolved after remaining open for 28 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Aristotle, GPT-5.5 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 20 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: Aristotle, GPT-5.5 Pro
Verification: Erdős Problems site confirmed
Open for: 28 years
Research activity: 2/5

26 Apr 2026Number Theory

Erdős Problem #896

Problem statement

For

A,B\subseteq[1,N]

, how many integers can have exactly one factorization

m=ab

with

a\in A

and

b\in B

The problem was resolved after remaining open for 54 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.5 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 1 problem-page discussion comment were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: GPT-5.5 Pro
Verification: Erdős Problems site confirmed
Open for: 54 years
Research activity: 1/5

26 Dec 2025Number Theory

Erdős Problem #897

Problem statement

If an additive function satisfies

\limsup_{p,k}f(p^k)/\log p^k=\infty

, must

\limsup_n(f(n+1)-f(n))/\log n=\infty

? Or even

\limsup_n f(n+1)/f(n)=\infty

Wirsing published the counterexample in 1981. The 2025 AI work rediscovered the construction and produced a Lean verification.

Details and sources

AI contribution

Archivara, Aristotle is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 28 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

The formal proof is new; the underlying counterexample is not.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Known counterexample formalized

System: Archivara, Aristotle
Verification: Lean checked
Open for: Known by 1981
Research activity: 3/5

21 Jun 2026Number Theory, Ramsey Theory

Erdős Problem #948

Problem statement

Can one choose a function

f

and a number of colours

k

so that every

k

-colouring of the integers contains a slowly growing sequence whose finite subset sums omit at least one colour?

The problem was resolved after remaining open for 49 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Aristotle, GPT-5.5 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 12 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: Aristotle, GPT-5.5 Pro
Verification: Lean checked
Open for: 49 years
Research activity: 2/5

25 Apr 2026Number Theory, Primes

Erdős Problem #1138

Problem statement

Let

x/2<y<x

C>1

, and let

d

be the largest prime gap below

x

. Must

\pi(y+Cd)-\pi(y)\sim Cd/\log y

The problem was disproved after remaining open for 27 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.5 Pro, GPT-5.5 Thinking is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 0 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Conjecture disproved

System: GPT-5.5 Pro, GPT-5.5 Thinking
Verification: Lean checked
Open for: 27 years
Research activity: 1/5

9 Apr 2026Number Theory, Primes

Erdős Problem #1141

Problem statement

Are there infinitely many

n

such that

n-k^2

is prime for every

k

coprime to

n

with

k^2<n

The problem was disproved after remaining open for 27 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

OpenAI internal model is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 5 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Conjecture disproved

System: OpenAI internal model
Verification: Lean checked
Open for: 27 years
Research activity: 1/5

16 Mar 2026Number Theory

Erdős Problem #1148

Problem statement

Can every sufficiently large integer

n

be represented as

x^2+y^2-z^2

with each of

x^2,y^2,z^2

at most

n

The problem was proved after remaining open for 27 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

Gemini 3 Pro, Gemini 3.1 Pro, GPT-5.2 Pro, GPT-5.2 Thinking, GPT-5.4 Pro is credited on the public resolution record.

Verification

Lean checked

Publication

Erdős Problems record and community AI ledger

Activity evidence

1 cited source record and 4 problem-page discussion comments were located. The score is a conservative proxy for documented research attention.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: Gemini 3 Pro, Gemini 3.1 Pro, GPT-5.2 Pro, GPT-5.2 Thinking, GPT-5.4 Pro
Verification: Lean checked
Open for: 27 years
Research activity: 1/5

1 Apr 2026Number Theory, Primes

Erdős Problem #1202

Problem statement

Given

\epsilon,\eta>0

, does some

k

force the following? For any primes

p_1<\cdots<p_k<n^{1-\epsilon}

and any choice of

(p_j-1)/2

residue classes modulo each

p_j

, fewer than

\epsilon n

integers

m\leq n

avoid all the chosen classes.

The problem was resolved after remaining open for 46 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.4 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

Specialist sieve question with limited prior dedicated literature.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem resolved

System: GPT-5.4 Pro
Verification: Erdős Problems site confirmed
Open for: 46 years
Research activity: 2/5

16 Apr 2026Number Theory, Divisors, Primitive Sets

Erdős Problem #1217

Problem statement

Let

A=\{a_1<a_2<\cdots\}

have positive lower logarithmic density. Must it contain a divisibility chain

a_{n_i}\mid a_{n_{i+1}}

such that

\limsup_{x\to\infty}\frac{\#\{i:a_{n_i}<x\}}{\log\log x}\geq\limsup_{x\to\infty}\frac{1}{\log\log x}\sum_{a_n<x}\frac{1}{a_n\log a_n}\,?

The problem was proved after remaining open for 60 years. The community trackers classify the result as a full resolution.

Details and sources

AI contribution

GPT-5.4 Pro is credited on the public resolution record.

Verification

Erdős Problems site confirmed

Publication

Erdős Problems record and community AI ledger

Activity evidence

Sustained primitive-set literature with multiple substantial advances.

This entry follows the full-resolution classification in the public trackers. The displayed statement is taken from the problem record; the primary page gives the proof links and literature notes.

Problem and proof record Discussion thread VibeMathed verification Community AI ledger

Problem proved

System: GPT-5.4 Pro
Verification: Erdős Problems site confirmed
Open for: 60 years
Research activity: 4/5

Probability & statistics

30 Jan 2026Random polynomials and probability

Erdős Problem #524 — random Littlewood-polynomial maxima

Problem statement

For i.i.d. Rademacher signs

a_k(t)=(-1)^{\epsilon_k(t)}

, determine the almost-sure order of

M_n(t)=\max_{x\in[-1,1]}\left|\sum_{k=1}^n a_k(t)x^k\right|.

An AI-assisted write-up obtained the sharp almost-sure limsup law and the correct stretched-exponential scale for the lower envelope. It did not determine the exact lower-envelope constant; independent human work subsequently proved the stronger exact result.

Details and sources

AI contribution

After Mehtaab Sawhney outlined the key Gaussian-process reduction, GPT-5.2 completed most of the argument with smaller inputs from Gemini and Grok.

Verification

Specialist checked; stronger paper followed

Publication

Public Erdős Problems discussion, community AI ledger, and a later stronger arXiv proof

Activity evidence

A Salem–Zygmund problem with classical partial bounds, a detailed 2026 community discussion, and a subsequent sharp human proof.

This remains a partial AI contribution, not an AI resolution of the full problem. Sawhney confirmed the stated partial argument, while joint work with Brayden Letwin later determined the exact lower-envelope constant.

Primary problem record AI contribution and expert discussion Community AI ledger Later stronger human proof

Correct partial result

System: GPT-5.2 / Gemini / Grok
Verification: Specialist checked; stronger paper followed
Open for: 72 years
Research activity: 3/5

12 May 2026Entropy and heat flow

Gaussian completely monotone conjecture

Problem statement

Must every time derivative of entropy along the heat flow obey the alternating-sign inequalities predicted by the Gaussian completely monotone conjecture?

Gu and Sellke exhibit an explicit probability measure on the real line whose fifth entropy derivative along heat flow has the forbidden sign. The example also refutes the associated McKean and Toscani conjectures.

Details and sources

AI contribution

The paper states that GPT-5.5 Pro found the explicit counterexample; the authors supplied and checked the proof.

Verification

Author-checked preprint

Publication

Complete public arXiv proof

Activity evidence

The conjecture sits inside a long, internationally active program on entropy, Fisher information, and Gaussian optimality; one consequence had remained open since 1966.

The direct target dates to Cheng and Geng’s 2015 conjecture. Its failure also settles a consequence of McKean’s 1966 Gaussian-optimality proposal.

Research paper Readable full paper

Conjecture disproved

System: GPT-5.5 Pro
Verification: Author-checked preprint
Open for: 11 years
Research activity: 4/5

18 May 2026Information theory

Log-convexity of Fisher information along heat flow

Problem statement

For every smooth positive density

f

\mathbb{R}^d

, must the Fisher information

t\mapsto I(f*\gamma_t)

be log-convex along the heat flow?

A smooth positive Gaussian-decaying density on the plane gives a hexagonal counterexample. Tensorization disproves the Cheng–Geng conjecture in every dimension at least two.

Details and sources

AI contribution

The authors report that GPT-5.5 Pro found the explicit two-dimensional counterexample.

Verification

Proof with explicit numerics

Publication

Public 28-page arXiv preprint

Activity evidence

A decade-old specialist conjecture embedded in an active information-theory literature, with less broad attention than the parent Gaussian-optimality program.

The paper combines an analytic construction with explicit two-dimensional numerical checks. It complements, rather than duplicates, the one-dimensional entropy counterexample.

Research paper Readable full paper

Conjecture disproved

System: GPT-5.5 Pro
Verification: Proof with explicit numerics
Open for: 11 years
Research activity: 3/5

10 Jun 2026Discrete probability and extremal combinatorics

Weighted Bernoulli sums above their mean

Problem statement

For nonnegative weights

w_i

with

\sum_i w_i=1

and independent

v_i\sim\mathrm{Bernoulli}(p)

, for which

p

does

\Pr[\sum_i w_i v_i\geq p]\geq p

hold for every choice of weights?

ProofCouncil correctly established several infinite families and counterexample ranges. Referees judged the mathematics genuinely novel and requested only minor revisions, while the full classification remains tied to difficult Manickam–Miklós–Singhi-type questions.

Details and sources

AI contribution

The multi-model harness discovered a new pairing argument for the family $p=2/k$ with $k\geq6$ and correctly handled several other parameter ranges.

Verification

Double-blind expert review; minor revisions

Publication

First Proof Second Batch report, complete submission, logs, and referee reports

Activity evidence

The question connects to the long-running Manickam–Miklós–Singhi conjecture and modern work on weighted Bernoulli sums.

This is recorded as partial rather than resolved because the broad 'for which values of p?' classification is not complete. The referee report nevertheless identifies genuinely new correct mathematics.

First Proof benchmark and source files Official report and referee decisions Problems, submissions, reviews, and logs

Novel partial families proved

System: ProofCouncil (primarily GPT-5.5 Pro; auxiliary Gemini and Claude)
Verification: Double-blind expert review; minor revisions
Open for: Research classification remains open
Research activity: 4/5

10 Jun 2026Stochastic partial differential equations

Unique invariant measure for the skew stochastic heat equation

Problem statement

For the stochastic heat equation

\partial_tu=\tfrac12\partial_x^2u+\delta_0(u)+\dot W

[0,1]

with Dirichlet boundary conditions, does its Markov semigroup have at most one invariant probability measure?

ProofCouncil gave a correct and novel uniqueness proof. All three expert referees rated it essentially flawless; the proof obtained a stronger finite-time absolute-continuity step than the human solution.

Details and sources

AI contribution

The harness found a stochastic-sewing drift estimate and combined it with Girsanov and ergodic arguments in a route different from the authors' proof.

Verification

Three expert referees; essentially flawless

Publication

First Proof Second Batch report, complete submission, logs, and referee reports

Activity evidence

The authors built on several years of work on distributional-drift stochastic heat equations and reported needing four to five weeks for their proof.

The problem was solved but unpublished when given to the benchmark. This is one of the strongest independently reviewed cases in the index because the report explicitly identifies both correctness and novelty.

First Proof benchmark and source files Official report and referee decisions Problems, submissions, reviews, and logs

Research problem proved

System: ProofCouncil (primarily GPT-5.5 Pro; auxiliary Gemini and Claude)
Verification: Three expert referees; essentially flawless
Open for: Unpublished SPDE research problem
Research activity: 4/5

15 May 2026Probability on groups

Return probability for a lamplighter walk

Problem statement

For the switch–walk–switch lamplighter walk on

\mathbb{Z}_2\wr T_d

, prove the sharp asymptotic

p_{2n}(e,e)=\rho_d^{2n}\exp\!\left[-\bigl(\pi^2(\log(d-1))^2+o(1)\bigr)\frac{n}{\log^2 n}\right],\qquad \rho_d=\frac{2\sqrt{d-1}}{d}.

QED derived the sharp return-probability asymptotic for the switch–walk–switch walk on the lamplighter group over a regular tree. The contributing probability expert verified the proof.

Details and sources

AI contribution

A fully automatic decomposition, proof, and verification run used Codex with GPT-5.5 Pro and received no mathematical input beyond the statement.

Verification

Domain expert verified

Publication

Dedicated arXiv paper, public proof record, and expert comments

Activity evidence

An expert-contributed active-research question with a small specialist audience; its proof was judged a publishable, substantive probability result.

The expert assessed this as a solid specialist contribution comparable to work in the Electronic Journal of Probability or Proceedings of the AMS.

Research paper Proof and expert record QED system paper

Open problem proved

System: QED / GPT-5.5 Pro
Verification: Domain expert verified
Open for: Under 1 year
Research activity: 2/5

15 May 2026Probability on groups

Total variation for a lamplighter walk

Problem statement

For the switch–walk–switch walk on

\mathbb{Z}_2\wr\mathbb{Z}

, with starts

x=(\mathbf{0},0)

and

y=(\mathbf{0},2)

, prove

\lVert P_t^x-P_t^y\rVert_{\mathrm{TV}}\asymp t^{-1/2}.

QED proved the sharp order t^{-1/2} for the total-variation distance between two switch–walk–switch laws started two sites apart on the lamplighter group over the integers.

Details and sources

AI contribution

The multi-agent system autonomously changed proof plans over several rounds before producing the expert-accepted argument.

Verification

Domain expert verified

Publication

Public problem, final proof, workflow, and expert comments

Activity evidence

A newly contributed active-research problem with real technical depth, but no evidence of a large pre-existing research program.

The contributor described this as a technically nontrivial PhD-level probability problem.

Proof and expert record QED system paper

Open problem proved

System: QED / GPT-5.5
Verification: Domain expert verified
Open for: Under 1 year
Research activity: 2/5

3 Sep 2025Probability theory

Quantitative two-chaos fourth-moment theorem

Problem statement

Can the qualitative fourth-moment theorem for sums of two Wiener–Itô integrals of different parity be strengthened to an explicit total-variation rate depending only on the fourth cumulant, and can an analogous theorem be established on Poisson space?

GPT-5 helped turn a qualitative fourth-moment theorem into an explicit total-variation convergence bound and extend the analysis to Poisson chaos, including a counterexample showing the added conditions are essentially necessary.

Details and sources

AI contribution

The model supplied the main proof structure and calculations after iterative correction and targeted hints from the authors.

Verification

Expert authors checked

Publication

Full arXiv paper with proofs and screenshots of both sessions

Activity evidence

The authors say the precise quantitative question had simply not been addressed before; it was not a longstanding focus of active competition.

The authors explicitly describe this as incremental and heavily human-guided: GPT-5 made a serious error in the Gaussian proof and missed a key positivity fact in the Poisson case until directed to it.

Research paper and interaction annex

Quantitative extension proved

System: GPT-5
Verification: Expert authors checked
Open for: Previously unstudied
Research activity: 1/5

21 Jul 2026Probability and statistics

Strong log-concavity of Chernoff’s density

Problem statement

Is the density f of argmaxₜ{W(t)−t²}, for two-sided Brownian motion W, strongly log-concave?

A concise proof establishes that the density of the Chernoff random variable is strongly log-concave, resolving the 2014 conjecture of Balabdaoui and Wellner.

Details and sources

AI contribution

The authors state that the mathematical proof was generated in its entirety by GPT-5.6 Sol.

Verification

Author checked; preprint public

Publication

Public arXiv note; journal review pending

Activity evidence

A documented 2014 conjecture in an active specialist area, with focused rather than field-wide attention.

This is a compact specialist result in shape-constrained probability. The evidence is the complete public proof and the authors’ explicit AI disclosure, not a proof-assistant certificate.

Preprint

Conjecture proved in preprint

System: GPT-5.6 Sol
Verification: Author checked; preprint public
Open for: 12 years
Research activity: 3/5

13 Jul 2026Statistics theory

Benjamini–Hochberg under correlated Gaussian tests

Problem statement

Does the Benjamini–Hochberg procedure always control false-discovery rate at its nominal level for correlated two-sided Gaussian p-values?

A correlated Gaussian factor model gives false-discovery rate above the nominal level, with a rigorous interval-arithmetic certificate valid for all sufficiently large numbers of hypotheses.

Details and sources

AI contribution

Edgar Dobriban reports that GPT-5.6 Pro obtained the proof, which he then checked carefully.

Verification

Author checked + interval certificate

Publication

Public arXiv preprint; journal review pending

Activity evidence

A widely believed question about a foundational multiple-testing procedure, with sustained work on dependence conditions.

The counterexample is narrower than a failure of the Benjamini–Hochberg procedure in every dependence model: it concerns correlated two-sided Gaussian tests.

Preprint and certificate

Twenty-year conjecture disproved

System: GPT-5.6 Pro
Verification: Author checked + interval certificate
Open for: 20 years
Research activity: 4/5

Quantum information & computing

21 May 2026Quantum optics and graph amplitudes

Four-particle monochromatic quantum graphs for all $D\geq4$

Problem statement

For four particles and local dimension

D\geq4

, can a complete edge-coloured, complex-weighted graph have unit amplitude for every monochromatic inherited colouring and zero amplitude for every nonmonochromatic colouring?

AlphaProof Nexus proves that no complex-weighted monochromatic quantum graph exists with $N=4$ particles in any local dimension $D\geq4$ . The formal development also derives the corresponding real-, integer-, and trinary-weight nonexistence results.

Details and sources

AI contribution

The proof-search system generated the algebraic nonexistence argument and a complete Lean proof for this parameter family.

Verification

Lean checked

Publication

AP Nexus preprint and public Lean proof

Activity evidence

The family belongs to an active graph-theoretic program for constructing high-dimensional entangled photonic states.

This is distinct from the already indexed diagonal family $N=D$ : it fixes $N=4$ and resolves every $D\geq4$ . The full two-parameter classification remains open.

AP Nexus paper Lean proof and problem audit Origin paper

Second infinite parameter family ruled out

System: AlphaProof Nexus
Verification: Lean checked
Open for: Studied since 2017–2018
Research activity: 3/5

18 May 2026Distributed photonic quantum computing

Non-local photonic SWAP, CNOT, Toffoli, and Fredkin gates

Problem statement

Can essential multiphoton gates be implemented non-locally between spatially separated photons without sending the photons to one location, pre-sharing entanglement, or performing Bell-state measurements?

AI-Mandel and PyTheus produced concrete qubit and qudit gate blueprints in which spatially separated photons need neither pre-shared entanglement nor Bell-state measurements. The constructions instead use path identity and quantum erasure, and include a new teleportation-like mechanism.

Details and sources

AI contribution

AI-Mandel proposed the underlying research idea and translated it into PyTheus searches. PyTheus found the concrete gates; the human authors interpreted and generalized the resulting mechanisms.

Verification

Peer-reviewed analytical construction

Publication

Physical Review Research letter with public preprint

Activity evidence

Non-local gates and distributed quantum information processing are active research areas with direct relevance to quantum networks.

The paper verifies the gate action analytically and gives experimental blueprints. It does not report a laboratory realization, so the record concerns the construction problem rather than hardware validation.

Peer-reviewed paper Public preprint AI-Mandel provenance paper PyTheus source code

Constructive gate architectures found

System: AI-Mandel multi-agent LLM + PyTheus
Verification: Peer-reviewed analytical construction
Research activity: 4/5

19 Feb 2026Quantum experiment program synthesis

Meta-solutions for quantum-state experiment families

Problem statement

Can one automatically discover a human-readable program that generates correct quantum-optical experiments for every size in a state family, including families for which no construction rule was previously known?

A transformer trained on synthetic state–experiment pairs generated readable Python programs that construct correct experimental setups for six target quantum-state families. The successful programs extrapolate beyond the training sizes and include previously unknown generalizations.

Details and sources

AI contribution

The model synthesized programs representing construction rules for entire infinite families, rather than optimizing one experimental setup at a time.

Verification

Peer reviewed; code and checkpoints released

Publication

Nature Machine Intelligence article with open artifacts

Activity evidence

Interpretable automated experiment design connects quantum optics, program synthesis, and scientific machine learning.

The authors tested twenty target classes: six were solved perfectly, while several other outputs matched only the initial sizes. This entry records the successful families and does not treat the remaining targets as solved.

Peer-reviewed article Public preprint Code repository

Six of twenty target families solved

System: Meta-design sequence-to-sequence transformer
Verification: Peer reviewed; code and checkpoints released
Research activity: 4/5

31 Jul 2020Photonic quantum gates

High-dimensional multipartite quantum transformations

Problem statement

How can one manipulate and control the general case of

n

-photon,

d

-dimensional quantum states with experimentally meaningful photonic transformations?

MELVIN uncovered the seed architectures for arbitrary high-dimensional multiphotonic transformations. The resulting scheme encodes a transformation in an ancillary state and uses a new high-dimensional quantum non-demolition measurement to mediate the operation.

Details and sources

AI contribution

MELVIN searched an estimated $10^{30}$ – $10^{40}$ optical setups and exposed the core pattern; the researchers then interpreted and generalized it into the published construction.

Verification

Peer-reviewed analytical proposal

Publication

Physical Review Letters paper and public preprint

Activity evidence

High-dimensional photonic gates are a central resource problem for quantum communication and information processing.

The construction addresses the previously open general $n$ -photon, $d$ -dimensional transformation setting. Several proposed instances are feasible with contemporary optics, but the paper is a theoretical blueprint rather than a universal laboratory demonstration.

Research paper Journal record MELVIN implementation

General constructive blueprint proposed

System: MELVIN
Verification: Peer-reviewed analytical proposal
Research activity: 4/5

24 Jul 2023Quantum retrodiction and communication

High-dimensional Mean King’s Problem

Problem statement

Can the Mean King’s quantum retrodiction puzzle be implemented beyond qubits with a scalable photonic scheme that retains a clear advantage over the best classical strategy?

PyTheus found graph-based optical setups for the Mean King’s Problem in dimensions $D=3,5,7$ . The researchers extracted a general prime-dimensional scheme whose reported success probabilities beat the classical $1/D$ benchmark by more than a factor of two.

Details and sources

AI contribution

The search system produced specific interpretable experiment graphs; the human researchers recognized and generalized their common construction.

Verification

Peer-reviewed proposal with numerical analysis

Publication

Optica Quantum article and public preprint

Activity evidence

The Mean King’s Problem is a long-running quantum-information puzzle; the high-dimensional experimental realization is a narrower specialist program.

This solves the experimental-design problem for a useful probabilistic scheme in prime dimensions; it is not a deterministic realization, and the reported setups had not yet been built in the laboratory.

Research paper Peer-reviewed article PyTheus source code

Prime-dimensional experimental scheme found

System: PyTheus
Verification: Peer-reviewed proposal with numerical analysis
Research activity: 3/5

13 Oct 2022Logic AI and quantum experiment design

SAT synthesis of photonic state-preparation experiments

Problem statement

Can the search for an interpretable photonic experiment that prepares a prescribed quantum state be formulated and solved exactly, rather than relying only on continuous optimization and local minima?

Klaus maps preparation of a target photonic quantum state to Boolean satisfiability, finds interpretable optical graphs, and iteratively removes unnecessary resources. Combining its exact logic search with numerical optimization improved the state-preparation designs studied in the paper.

Details and sources

AI contribution

The system converts physical constraints into SAT clauses, returns exact satisfying designs, and supplies unsatisfiability evidence within the encoded resource class.

Verification

Peer-reviewed exact method

Publication

Quantum journal article and public preprint

Activity evidence

Exact synthesis of photonic experiments is an active bridge between quantum optics, Boolean satisfiability, and automated scientific design.

This is an exact algorithmic resolution of encoded state-preparation instances, not a proof that every quantum state has a feasible experiment under arbitrary laboratory constraints.

Peer-reviewed article Public preprint

Exact synthesis framework demonstrated

System: Klaus logic AI
Verification: Peer-reviewed exact method
Research activity: 3/5

21 May 2026Quantum optics and graph amplitudes

Monochromatic quantum graphs in the diagonal family

Problem statement

Can a complete edge-coloured, complex-weighted graph be chosen so that perfect-matching amplitudes equal one for every monochromatic inherited vertex colouring and vanish for every nonmonochromatic colouring? The proved nonexistence family has even

N=D\geq4

AlphaProof Nexus proves nonexistence in the diagonal family $N=D$ for every even $N\geq4$ , alongside additional finite parameter cases. The broader two-parameter problem remains open.

Details and sources

AI contribution

The system generated algebraic nonexistence arguments for several parameter families and formalized them in Lean.

Verification

Lean checked

Publication

AP Nexus preprint and public Lean folder

Activity evidence

A specialist quantum-optics problem with several papers and public problem discussions over roughly eight years.

This settles an infinite diagonal family, not the complete $N,D$ classification sought by the parent quantum-optics problem.

AP Nexus paper Origin paper Lean artifacts

Infinite parameter family ruled out

System: AlphaProof Nexus
Verification: Lean checked
Open for: Studied since 2017–2018
Research activity: 3/5

29 Jun 2026Quantum optimization

FGG conjecture for QAOA on the ring of disagrees

Problem statement

For an even cycle of size

N

and depth

p

satisfying

2p+2\leq N

, is the optimal QAOA approximation ratio for MaxCut exactly

\frac{2p+1}{2p+2}\,?

Claude Fable 5 found a dynamical-symmetry and quantum-signal-processing argument proving the exact optimal depth-p QAOA ratio on an even cycle. The complete proof was checked by the Lean 4 kernel.

Details and sources

AI contribution

After humans formalized the definitions and isolated the open gap, the model supplied the decisive construction and completed the formal proof through an interactive Lean loop.

Verification

Lean checked end to end

Publication

Public arXiv paper and complete Lean development

Activity evidence

The conjecture dates to the original 2014 QAOA analysis. It had proofs only at small depth and numerical confirmation through larger p inside a heavily studied quantum-optimization program.

Humans audited that the fixed Lean statement faithfully represents the mathematical conjecture. The proof itself compiles using the standard classical axioms in Mathlib.

Paper and formal-verification record Readable full paper

Conjecture proved

System: Claude Fable 5
Verification: Lean checked end to end
Open for: 12 years
Research activity: 4/5

Theoretical computer science

10 Jun 2026Computability theory and model theory

Nonuniform definability of automorphisms

Problem statement

Does there exist a computably represented countable structure

A

that is computably AUT-countable on a cone, but for every finite parameter tuple

\bar a

has an automorphism

\pi

that is not

\Sigma^\mathrm{in}_1

-definable from

\bar a\cup\pi(\bar a)

Three systems produced mathematically correct constructions. The First Proof editors rated all three as requiring only minor revisions, chiefly because of missing citations rather than gaps in the argument.

Details and sources

AI contribution

ProofCouncil, the UCLA Moonshot harness, and ChatGPT 5.5 Pro independently generated solutions in the controlled one-shot benchmark.

Verification

Double-blind expert review; minor revisions

Publication

First Proof Second Batch report, complete submissions, logs, and referee reports

Activity evidence

The problem connects active work on computable structure theory, automorphism groups, and definability; its authors reported that the example took several days to find.

This was a solved but unpublished research problem supplied by its authors, not a decades-old public conjecture. The mathematics passed expert review, while the reports flag serious attribution omissions in several submissions.

First Proof benchmark and source files Official report and referee decisions Problems, submissions, reviews, and logs

Research problem proved

System: GPT-5.5 Pro / ProofCouncil / UCLA Moonshot
Verification: Double-blind expert review; minor revisions
Open for: Unpublished research problem
Research activity: 3/5

Algorithms

15 Jul 2026Analog computation and reaction networks

Chemical reaction networks and CRN-computable reals

Problem statement

Can the central equivalence and universality results connecting polynomial ODEs, chemical reaction networks, linear production protocols, and stochastic mean-field limits be assembled in one machine-checked framework?

Ripple assembles a sorry-free Lean 4 development of CRN-computable reals, polynomial-ODE and LPP compilation, stochastic mean-field limits, and deterministic and stochastic Turing-completeness. The project repairs gaps exposed during formalization and adds a checked construction showing that ζ(3) is CRN-computable.

Details and sources

AI contribution

The authors used the models to translate, repair, and extend the mathematical development inside an iterative Lean verification loop.

Verification

Lean checked; no sorry

Publication

Public arXiv paper and Lean repository

Activity evidence

The work connects several active literatures in analog computation, reaction-network theory, and mechanized mathematics, but formalizes a focused technical program.

This is a formalization and repair record, not a claim that every theorem in the framework was first discovered by AI. The paper reports only the foundational axioms already used by Mathlib.

Research paper Lean repository

Theory formalized and gaps repaired

System: Claude Opus 4.6–4.8 / Claude Fable 5 / GPT-5.4–5.6
Verification: Lean checked; no sorry
Research activity: 3/5

8 Apr 2026Learning dynamics

Exhaustive AdaBoost cycling question

Problem statement

For every finite training set, does exhaustive AdaBoost eventually converge to a finite cycle of weak classifiers and weight vectors?

Wang constructs a finite exhaustive-AdaBoost instance whose orbit never becomes periodic, resolving a question posed by Rudin, Schapire, and Daubechies in 2012.

Details and sources

AI contribution

The author credits both models as collaborators in developing the block-product counterexample and its proof.

Verification

Exact rational certificate

Publication

Public computer-assisted arXiv proof

Activity evidence

A standing theoretical-machine-learning question from COLT 2012 with a sustained specialist thread on AdaBoost dynamics.

Every asserted computation is certified with exact rational arithmetic; the nonperiodicity argument uses an irrational logarithmic ratio.

Research paper Readable full paper

Question answered negatively

System: GPT-5.4 Pro / Claude Opus 4.6
Verification: Exact rational certificate
Open for: 14 years
Research activity: 3/5

5 Jul 2026Discrepancy theory and algorithms

Optimal online discrepancy in linear time

Problem statement

Given online vectors

v_t\in\mathbb{R}^d

with

\lVert v_t\rVert_2\leq1

, can signs

\varepsilon_t\in\{-1,1\}

be chosen in

O(dT)

time so that every prefix has

\ell_\infty

discrepancy

O(\sqrt{\log T})

with high probability?

Aden-Ali gives an $O(dT)$ -time online algorithm attaining the optimal $O(\!\sqrt{\log T}\!)$ prefix-discrepancy bound, replacing an earlier algorithm exponential in both $T$ and $d$ .

Details and sources

AI contribution

The paper states that the model conversation discovered both the algorithm and the main proof after the author supplied the research prompt.

Verification

Author-checked preprint

Publication

Public eight-page arXiv proof

Activity evidence

Online vector balancing and discrepancy minimization are internationally active areas; the target matched a known optimal bound but required an efficient construction.

This closes a computational-efficiency gap around an already optimal discrepancy bound; it is not a new improvement to the asymptotic bound itself.

Research paper

Runtime gap closed

System: GPT-5.5 Pro Extended
Verification: Author-checked preprint
Open for: Long-standing runtime gap
Research activity: 4/5

28 May 2026Randomized graph algorithms

Nearly uniform sampling of directed Eulerian tours

Problem statement

Does the proposed flip–repair Markov chain mix rapidly enough to yield a nearly uniform directed-Eulerian-tour sampler in

\widetilde O(m^{3/2})

worst-case time?

Anari gives a worst-case $\widetilde O(m^{3/2})$ sampler for nearly uniform directed Eulerian tours, breaking the previous $mn$ -type barrier on sparse graphs.

Details and sources

AI contribution

The author devised the algorithmic plan and conjectured the key mixing theorem; GPT-5.5 Pro Extended supplied its linear-algebra proof, while Codex assisted manuscript assembly.

Verification

Author-checked preprint

Publication

Public 42-page arXiv proof

Activity evidence

Eulerian-tour sampling sits in an active algorithms-and-probability literature, while the exact mixing statement was newly isolated by the author.

The AI-resolved object is the author’s mixing conjecture inside a broader new algorithm, not a previously named community conjecture.

Research paper

Conjectured mixing theorem proved

System: GPT-5.5 Pro Extended / Codex
Verification: Author-checked preprint
Open for: Research bottleneck posed during the project
Research activity: 3/5

4 Apr 2026Convex–concave optimization

Last-iterate rate for anchored gradient descent–ascent

Problem statement

For a monotone

K

-Lipschitz saddle operator arising from a smooth convex–concave min–max problem, can anchored gradient descent–ascent be scheduled so that its exact last-iterate squared-gradient residual is

O(1/t)

A new anchoring schedule gives squared-gradient residual $O(1/t)$ for smooth convex–concave min–max problems, closing the rate gap left by the 2019 analysis.

Details and sources

AI contribution

The model and human researchers jointly discovered the schedule and the discrete-recurrence argument; Nexus produced the checked formal proof.

Verification

Lean checked

Publication

Standalone public preprint and Lean source

Activity evidence

A sustained specialist line in minimax optimization with published precursor and follow-up analyses.

The prior method obtained exponents approaching but not reaching the exact $O(1/t)$ squared-residual rate.

Research paper Lean proof 2019 precursor

Optimal rate attained

System: AlphaProof Nexus
Verification: Lean checked
Open for: 7 years
Research activity: 3/5

9 Jul 2026Planar graph algorithms

Minimum edge-outerplanar embedding

Problem statement

Can the minimum edge-outerplanarity of a finite loopless planar graph—minimized over all planar embeddings—be computed in polynomial time?

A polynomial-time algorithm now computes a planar embedding of minimum edge-outerplanarity for every finite loopless planar graph, resolving Bentz’s 2009 question.

Details and sources

AI contribution

GPT-5.5 Pro produced the initial proof in a solver–verifier pipeline; Hantao Yu then manually checked and polished it.

Verification

Author checked and polished

Publication

Complete public arXiv proof and open solver–verifier pipeline

Activity evidence

A documented 2009 specialist problem with a modest chain of related planar-embedding work, rather than broad sustained activity.

Edge-outerplanarity counts the rounds needed to delete every edge incident with the current outer face. This result concerns choosing the optimal embedding, not merely evaluating a fixed one.

Research paper Solver–verifier pipeline

Open problem proved

System: GPT-5.5 Pro
Verification: Author checked and polished
Open for: 17 years
Research activity: 2/5

22 Sep 2025Combinatorial optimization

Bicriteria submodular maximization over $p$ -systems

Problem statement

Does the greedy algorithm for monotone submodular maximization over a

p

-system achieve a

(1-\varepsilon,\lceil\log_{p+1}(1/\varepsilon)\rceil)

bicriteria approximation? If not, determine the correct dependence on

p

GPT-5 noticed that the proposed infeasibility ratio worsened in the wrong direction as p increased, and derived the essentially correct replacement bound based on log base 1 + 1/p.

Details and sources

AI contribution

Given two source papers and the newly formulated conjecture, the model produced the corrected theorem and a basically correct proof with minor repairable errors.

Verification

Authors checked in detail

Publication

Gödel Test arXiv report reproducing the prompt, answer, and line-by-line evaluation

Activity evidence

The authors formulated this conjecture specifically for a controlled model test; it had no prior community research history.

This was a newly designed test conjecture, not a famous longstanding problem. The authors report one erroneous intermediate inequality, but confirm that the claimed corrected guarantee follows directly.

Gödel Test paper

Conjecture refuted; corrected bound proved

System: GPT-5
Verification: Authors checked in detail
Open for: Newly posed
Research activity: 1/5

22 Jul 2026Combinatorial optimization

Dinitz–Garg–Goemans Conjecture

Problem statement

Can every fractional single-source unsplittable flow be rounded without increasing either edge congestion or total cost?

A finite unsplittable-flow instance has fractional cost 58, while every admissible unsplittable flow costs at least 60, contradicting the proposed cost-preserving rounding theorem.

Details and sources

AI contribution

Dmitry Rybin reports that GPT-5.6 Pro searched for and produced the counterexample, exact data, exhaustive verification code, and proof certificate.

Verification

Public certificate; peer review pending

Publication

Public counterexample and complete ChatGPT conversation

Activity evidence

A recognized approximation-algorithms conjecture with substantial work on unsplittable-flow rounding.

The counterexample is explicit and computationally checkable, but no archival peer-reviewed paper or proof-assistant formalization was located at the time of this update.

Full ChatGPT conversation Author announcement Tracker record

Conjecture disproved

System: GPT-5.6 Pro
Verification: Public certificate; peer review pending
Open for: 27 years
Research activity: 4/5

14 Dec 2023Combinatorial optimization

FunSearch online bin-packing heuristics

Program search produced online bin-packing heuristics that improved the evaluated baselines, without resolving the general approximation theory of bin packing.

Details and sources

AI contribution

The language model mutated priority functions while an executable evaluator selected and evolved better programs.

Verification

Peer reviewed + executable artifacts

Publication

Nature paper and public notebooks

This is an algorithmic discovery rather than a proof of an open conjecture. It is separated from the cap-set entry because the evidence and mathematical claim are different.

Nature paper Executable repository

New heuristics discovered

System: FunSearch / Codey
Verification: Peer reviewed + executable artifacts

14 May 2025Algebraic complexity

$4\times4$ complex matrix multiplication

AlphaEvolve found a construction multiplying two 4 × 4 complex matrices with 48 scalar multiplications, improving on the 49 from recursive Strassen.

Details and sources

AI contribution

Gemini-generated programs were evolved against exact algebraic evaluators until a lower-rank construction was found.

Verification

Executable certificate + expert analysis

Publication

Public technical report and selected artifacts

This resolves a specific finite construction record, not the asymptotic matrix-multiplication exponent or matrix multiplication over every field.

AlphaEvolve paper Official account

Multiplication count improved

System: AlphaEvolve / Gemini
Verification: Executable certificate + expert analysis

Open Math Problems Claimed to Be Solved with AI

Log-concavity of codimension-three pure O-sequences

Hook coefficients of universal Hilbert series

Solubilizer Conjecture A.1

Solubilizer Conjecture A.13

Solubilizer Conjecture A.16

Anderson’s quasi-completeness question

Fel’s conjecture on syzygies

Carbery’s almost-orthogonality inequality in LpL^pLp

Single-minus gluon tree amplitudes

Erdős Problem #1040 — polynomial sublevel-set measure

Neural Jacobian Conjecture at width N=n+1N=n+1N=n+1

Equilibria of the Vlasov–Maxwell–Landau system

Erdős Problem #1039 — inradius of polynomial lemniscates

Derivative bounds for polynomial lemniscates

Projection lengths of polynomial lemniscates

Convexity of small lemniscate components

Diameter of a lemniscate component

Entire functions preserving rationality

Prescribed derivative-zero sets

FullRSB jamming identity a+b=1a+b=1a+b=1

First Proof Problem 2 — uniform Whittaker test vector

Erdős Problem #1038 — polynomial lemniscates

Lower bounds for advection–diffusion

Cosmic-string radiation integral

Ran–Teng Conjecture 20

Erdős Problem #1153

Effective Brascamp–Lieb inequalities

Erdős Problem #987

Erdős Problem #990

Erdős Problem #997

Erdős Problem #1195

Erdős Problem #1197

Graffiti Conjecture 284

Multivariate independence-polynomial lower bound

Hamilton decompositions of the directed 3-torus

Ramsey numbers for book graphs

Diagonal Ramsey upper-bound constant

Erdős Problem #138 — gaps between van der Waerden numbers

Written on the Wall II, Graph Conjecture 2

Ben Green’s Open Problem 57

Record compositions of alternating permutations

Reciprocals of partition polynomials

Weak bipartite reconstruction with distinct vertex types

Erdős Problem #1032 — minimum degree in 4-critical graphs

Erdős Problem #176 — discrepancy on arithmetic progressions

Pentagons in triangle-free graphs

Distinct consecutive sums of permutations

Cycle lengths in arithmetic progressions

Triangle-free graph completion to diameter two

Growth rate of minimal graph cuts

Equidistribution of dense Sidon sumsets

Countable simultaneous discrepancy

Monochromatic collinear sets

Abelian-square-free lattice walks

Monotone progressions in an ordering of the reals

Progression-free sets and their complements

Partitioning bounded-representation sets

Difference collisions at square-root density

Erdős Problem #501 — relative independence under a measure extension

Erdős Problem #1033 — triangle degree-sum bound

Erdős Problem #593 — obligatory triple systems

Erdős Problem #1177 — exact avoidance spectra

Graffiti Conjecture 143

Graffiti Conjecture 154 under the standard-deviation reading

TxGraffiti–Davila Conjecture 9

Pandey parity conjecture for generalized Petersen graphs

Koch–Narayan Conjecture 1

Elizalde–Luo {1132,3312}\{1132,3312\}{1132,3312} pattern-avoidance conjecture

Kurkov’s Fubini-number sum conjecture

Erdős Problem #866 — eventual value of h4h_4h4​

Strong-majority 444-edge-coloring with at most two degree-333 vertices

Erdős Problem #43 — paired Sidon sets

Ramsey-style hypergraph construction

Cycle Double Cover Conjecture

Sabidussi compatibility conjecture

Erdős Problem #124

AlphaEvolve mathematics portfolio

GPT-5 “ten Erdős problems” claim

FunSearch cap-set constructions

Carbery’s almost-orthogonality inequality in $L^p$

Neural Jacobian Conjecture at width $N=n+1$

FullRSB jamming identity $a+b=1$

Elizalde–Luo $\{1132,3312\}$ pattern-avoidance conjecture

Erdős Problem #866 — eventual value of $h_4$

Strong-majority $4$ -edge-coloring with at most two degree- $3$ vertices

Erdős–Szemerédi sum–product conjecture over $\mathbb R$

Spin parity for $k$ -differentials

IRIS Conjecture 6.1 on simple $3$ -polytopes

Conant’s mod- $4$ Kawauchi conjecture