openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance

Frontier

Frontier API →

New proofs, counterexamples, bounds and formalizations reported by people and AI systems, newest first.

Reported developments, attributed to their sources. Inclusion is not an OpenMath assessment; evidence slots show what each source reports. Updated Oct 13, 2026.

April 2026 22

New proofCombinatoricsErdős #202

Erdős problem #202

Full solution. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Boon Suan Ho
LFCR
New proofCombinatoricsErdős #1190

Erdős problem #1190

Full solution. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Boon Suan Ho
LFCR
New proofCombinatoricsErdős #1014

Erdős problem #1014

Full solution. Contribution type: AI standalone.

OpenAI internal model
LFCR
New proofCombinatoricsErdős #863

Erdős problem #863

Full solution. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Boon Suan Ho
LFCR
New proofCombinatoricsErdős #996

Erdős problem #996

Full solution. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Boon Suan Ho
LFCR
New proofCombinatoricsErdős #610

Erdős problem #610

Full solution (Lean) (implicit in literature). Contribution type: AI collaborating with humans.

Aristotle · GPT-5.4 Pro · Przemek Chojecki
LFCR
New proofCombinatoricsErdős #603

Erdős problem #603

Full solution. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Przemek Chojecki
LFCR
New proofCombinatoricsErdős #1195

Erdős problem #1195

Full solution. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Boon Suan Ho
LFCR
New proofCombinatoricsErdős #741

Erdős problem #741

Full solution (Lean). Contribution type: AI standalone.

DeepMind prover agent
LFCR
New proofCombinatoricsErdős #1217

Erdős problem #1217

Full solution. Contribution type: AI standalone.

GPT-5.4 Pro
LFCR
New proofCombinatoricsErdős #1196

Erdős problem #1196

Full solution (stronger than literature). Contribution type: AI collaborating with humans.

GPT-5.4 Thinking · Nat Sothanaphan
LFCR
New proofCombinatoricsErdős #858

Erdős problem #858

Full solution. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Przemek Chojecki
LFCR
New proofCombinatoricsErdős #258

Erdős problem #258

Full solution. Contribution type: AI building on literature.

GPT-5.4 Pro
LFCR
New proofCombinatoricsErdős #1197

Erdős problem #1197

Full solution (Lean). Contribution type: AI building on literature.

Aristotle · Claude Opus 4.7 · GPT-5.4 Pro
LFCR
New proofCombinatoricsErdős #1196

Erdős problem #1196

Full solution. Contribution type: AI standalone.

GPT-5.4 Pro
LFCR
New proofCombinatoricsErdős #990

Erdős problem #990

Full solution. Contribution type: AI standalone.

OpenAI internal model
LFCR
New proofCombinatoricsErdős #987

Erdős problem #987

Full solution. Contribution type: AI standalone.

OpenAI internal model
LFCR
New proofCombinatoricsErdős #960

Erdős problem #960

Full solution. Contribution type: AI standalone.

OpenAI internal model
LFCR
New proofCombinatoricsErdős #1141

Erdős problem #1141

Full solution. Contribution type: AI standalone.

OpenAI internal model
LFCR
New proofCombinatoricsErdős #1091

Erdős problem #1091

Full solution. Contribution type: AI standalone.

OpenAI internal model
LFCR
New proofCombinatoricsErdős #152

Erdős problem #152

Full solution (Lean). Contribution type: AI alongside literature.

DeepMind prover agent
LFCR
New proofCombinatoricsErdős #1202

Erdős problem #1202

Full solution. Contribution type: AI standalone.

GPT-5.4 Pro
LFCR

March 2026 6

New proofCombinatoricsErdős #997

Erdős problem #997

Full solution. Contribution type: AI alongside literature.

OpenAI internal model
LFCR
New proofCombinatoricsErdős #380

Erdős problem #380

Full solution. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Terence Tao
LFCR
New proofCombinatoricsErdős #125

Erdős problem #125

Full solution (Lean). Contribution type: AI standalone.

DeepMind prover agent
LFCR
New proofCombinatoricsErdős #369

Erdős problem #369

Full solution. Contribution type: AI collaborating with humans.

GPT · Sky Yang
LFCR
New proofCombinatoricsErdős #650

Erdős problem #650

Full solution (stronger than literature). Contribution type: AI alongside literature.

GPT-5.4 Pro
LFCR
New proofCombinatoricsErdős #457

Erdős problem #457

Full solution (Lean). Contribution type: AI standalone.

Aristotle · GPT-5.2 Pro
LFCR

February 2026 12

New proofCombinatoricsErdős #966

Erdős problem #966

Full solution (Lean). Contribution type: AI building on literature.

Aristotle
LFCR
New proofCombinatoricsErdős #846

Erdős problem #846

Full solution (Lean); 🟢 Full solution. Contribution type: AI alongside literature.

DeepMind prover agent; OpenAI internal model (independently)
LFCR
New proofCombinatoricsErdős #851

Erdős problem #851

Full solution (building upon 🟡 Romanoff (1934)). Contribution type: AI alongside literature.

GPT-5.2 Pro
LFCR
New proofCombinatoricsErdős #659

Erdős problem #659

Full solution. Contribution type: AI alongside literature.

Aletheia
LFCR
New proofCombinatoricsErdős #397

Erdős problem #397

Full solution. Contribution type: AI alongside literature.

Aletheia
LFCR
New proofCombinatoricsErdős #1153

Erdős problem #1153

Full solution. Contribution type: AI collaborating with humans.

AlphaEvolve · Claude · Gemini Pro · GPT-5.2 Thinking · GPT-5.4 Pro · Aron Bhalla · Nat Sothanaphan · Terence Tao
LFCR
New proofTheoretical computer scienceGemini case 8.5

Networked information aggregation

Case 8.5 in the Gemini Deep Think research report (convergence bound).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 8.4

Revelation-principle domain extension

Case 8.4 in the Gemini Deep Think research report (hypothesis dependent extension).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 8.3

Self-regularized Gumbel sigmoid

Case 8.3 in the Gemini Deep Think research report (optimization analysis).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 8.2

Ratio difference maximization

Case 8.2 in the Gemini Deep Think research report (hardness reduction).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 8.1.2

Unsymmetrized / Li–Médard assertions

Case 8.1.2 in the Gemini Deep Think research report (scoped proof).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 8.1.1

Courtade–Kumar high-noise regime

Case 8.1.1 in the Gemini Deep Think research report (partial result).

Gemini Deep Think research version · Google DeepMind
LFCR