The Erdos

Math Emporium

“A mathematician is a machine for turning coffee into theorems.”— Paul Erdos

Explore the vast universe of mathematical knowledge rooted in the work of Paul Erdos. Navigate constellations of theorems, witness AI breakthroughs in formal mathematics, and contribute your own ideas to the frontier of human knowledge.

Explore the UniverseBrowse ProblemsJoin the Emporium

Live from the Erdos Problems Database — 1,212 problems tracked

1,212
Total Problems
653
Open
506
Proved/Solved
389
Lean Formalized
106
With Prizes

Data sourced from teorth/erdosproblems — maintained by Terence Tao & community

19
Featured
16
Solved
7
AI Contributed
7
Lean Proofs

North Stars — Featured Problems

Number TheorySOLVED

Erdos Problem #728

#728
a! b!∣n! (a+b−n)!withC1log⁡n<a+b−n<C2log⁡na!\, b! \mid n!\, (a+b-n)! \quad\text{with}\quad C_1 \log n < a+b-n < C_2 \log n
AI: GPT-5.2 Pro, Aristotle (Harmonic)
CombinatoricsSOLVED

Erdos Problem #125

#125
DeepMind prover: full solution in Lean\text{DeepMind prover: full solution in Lean}
AI: DeepMind Prover Agent
Number TheoryOPEN

Erdos-Straus Conjecture

4n=1x+1y+1z\frac{4}{n} = \frac{1}{x} + \frac{1}{y} + \frac{1}{z}
Number TheoryOPEN

Erdos Conjecture on Arithmetic Progressions

∑n∈A1n=∞  ⟹  A⊇AP of length k,  ∀k\sum_{n \in A} \frac{1}{n} = \infty \;\Longrightarrow\; A \supseteq \text{AP of length } k,\; \forall k
Number TheoryOPEN

Erdos-Turan Conjecture on Additive Bases

lim sup⁡n→∞rB,2(n)=∞\limsup_{n\to\infty} r_{B,2}(n) = \infty

AI Milestones in Erdos Problems

Erdos Problem #728Jan 6, 2026
GPT-5.2 Pro, Aristotle (Harmonic)
Erdos Problem #125Mar 30, 2026
DeepMind Prover Agent
Erdos Problem #205Jan 10, 2026
Aristotle, GPT-5.2 Thinking
Erdos Problem #457Mar 2, 2026
Aristotle, GPT-5.2 Pro
Erdos Problem #846Feb 21, 2026
DeepMind Prover Agent
Erdos Problem #347Oct 2025 - Feb 2026
Aristotle, Claude Opus, Codex, GPT
Erdos Problem #1051Jan 29, 2026
Aletheia

How It Works

Gemini Reasons

Google Gemini provides the mathematical intelligence — reasoning about conjectures, generating proof strategies, and exploring the problem space.

Fal Computes

fal.ai provides serverless compute for running Lean 4 proof verification, generating mathematical art, and powering ShinkaEvolve discovery instances.

Lean Verifies

Lean 4 is the formal verification backbone. Every claimed proof is checked by the Lean type checker — if it compiles, it's correct. No handwaving.