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 17

Partial resultCombinatoricsErdős #675

Erdős problem #675

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Boon Suan Ho
LFCR
Partial resultCombinatoricsErdős #976

Erdős problem #976

Conditional partial result. Contribution type: AI collaborating with humans.

GPT-5.4 · Aron Bhalla
LFCR
Partial resultCombinatoricsErdős #872

Erdős problem #872

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Om_Buddhdev_sensho
LFCR
Partial resultCombinatoricsErdős #852

Erdős problem #852

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 · Aron Bhalla
LFCR
Partial resultCombinatoricsErdős #251

Erdős problem #251

Solution to variant problem. Contribution type: AI standalone.

GPT-5.4 Pro
LFCR
Partial resultCombinatoricsErdős #1209

Erdős problem #1209

Partial result (Lean). Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Enrique Barschkis
LFCR
Partial resultCombinatoricsErdős #366

Erdős problem #366

Conditional partial result. Contribution type: AI alongside literature.

Automated research pipeline
LFCR
Partial resultCombinatoricsErdős #75

Erdős problem #75

Partial result. Contribution type: AI building on literature.

GPT-5.4 Pro
LFCR
Partial resultCombinatoricsErdős #138

Erdős problem #138

Partial result (Lean). Contribution type: AI standalone.

DeepMind prover agent
LFCR
Partial resultCombinatoricsErdős #138

Erdős problem #138

Partial result of variant problem. Contribution type: AI collaborating with humans.

GPT-5.4 Thinking · Nat Sothanaphan
LFCR
Partial resultCombinatoricsErdős #12

Erdős problem #12

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 Thinking · Nat Sothanaphan · Terence Tao
LFCR
Partial resultCombinatoricsErdős #12

Erdős problem #12

Partial result (Lean) (solutions to first part and second part). Contribution type: AI building on literature.

DeepMind prover agent
LFCR
Partial resultCombinatoricsErdős #26

Erdős problem #26

Solution to stronger problem. Contribution type: AI building on literature.

DeepMind prover agent
LFCR
Partial resultCombinatoricsErdős #396

Erdős problem #396

Related result. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · GPT-5.4 Thinking · Justin Dehorty · Nat Sothanaphan
LFCR
Partial resultCombinatoricsErdős #749

Erdős problem #749

Partial result; 🟡 Solution to variant problem. Contribution type: AI collaborating with humans.

GPT-5.4 Thinking · Aron Bhalla
LFCR
Partial resultCombinatoricsErdős #629

Erdős problem #629

Partial result. Contribution type: AI alongside literature.

Gemini 3.1 Pro · GPT-5.4 Thinking
LFCR
Partial resultCombinatoricsErdős #684

Erdős problem #684

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 Thinking · Nat Sothanaphan
LFCR

March 2026 18

Partial resultCombinatoricsErdős #741

Erdős problem #741

Partial result (solution to second part). Contribution type: AI standalone.

OpenAI internal model
LFCR
Partial resultCombinatoricsErdős #741

Erdős problem #741

Partial result (Lean) (solution to variant of first part; solution to second part). Contribution type: AI standalone.

DeepMind prover agent
LFCR
Partial resultCombinatoricsErdős #684

Erdős problem #684

Partial result. Contribution type: AI standalone.

OpenAI internal model
LFCR
Partial resultCombinatoricsErdős #374

Erdős problem #374

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Terence Tao
LFCR
Partial resultCombinatoricsErdős #396

Erdős problem #396

OEIS sequence. Contribution type: Computation.

Claude Opus 4.6 · Gemini 3.1 Deep Think · GPT-5.4 Pro
LFCR
Partial resultCombinatoricsErdős #488

Erdős problem #488

Partial result. Contribution type: AI collaborating with humans.

Aristotle · GPT-5.4 · Przemek Chojecki
LFCR
Partial resultCombinatoricsErdős #25

Erdős problem #25

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Przemek Chojecki
LFCR
Partial resultCombinatoricsErdős #1183

Erdős problem #1183

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Przemek Chojecki · Quanyu Tang
LFCR
Partial resultCombinatoricsErdős #396

Erdős problem #396

Partial result. Contribution type: AI collaborating with humans.

Claude · Codex · GPT · Malek Zribi
LFCR
Partial resultCombinatoricsErdős #120

Erdős problem #120

Solution to variant problem (Lean). Contribution type: AI alongside literature.

DeepMind prover agent
LFCR
Partial resultCombinatoricsErdős #1095

Erdős problem #1095

Partial result. Contribution type: AI collaborating with humans.

Claude Opus 4.6 · Gemini 3.1 Pro · GPT-5.4 Pro · shtuka
LFCR
Partial resultCombinatoricsErdős #931

Erdős problem #931

Partial result. Contribution type: AI collaborating with humans.

Claude · GPT-5.4 · Adenwalla · Malek Zribi
LFCR
Partial resultCombinatoricsErdős #423

Erdős problem #423

Partial result. Contribution type: AI collaborating with humans.

GPT-5.2 Thinking · GPT-5.4 Thinking · Quanyu Tang · Nat Sothanaphan
LFCR
Partial resultCombinatoricsErdős #349

Erdős problem #349

Improved partial result. Contribution type: AI building on literature.

GPT-5.2 Thinking
LFCR
Partial resultCombinatoricsErdős #650

Erdős problem #650

Numerical optimization. Contribution type: Computation.

AlphaEvolve
LFCR
Partial resultCombinatoricsErdős #1039

Erdős problem #1039

Partial result (Lean). Contribution type: AI collaborating with humans.

Aristotle · Claude Opus 4.6 · Houi
LFCR
Partial resultCombinatoricsErdős #848

Erdős problem #848

Derived explicit bound; 🟡 Partial result of variant problem. Contribution type: AI building on literature.

Gemini 3.1 Pro · GPT-5.2 Thinking · GPT-5.4 Thinking
LFCR
Partial resultCombinatoricsErdős #513

Erdős problem #513

Slight improvement to past construction. Contribution type: AI building on literature.

GPT-5.2 Thinking
LFCR

February 2026 5

Partial resultCombinatoricsErdős #1090

Erdős problem #1090

Proof found (Lean). Contribution type: AI building on literature.

Aristotle · Gemini 3 Flash
LFCR
Partial resultCombinatoricsErdős #125

Erdős problem #125

Solution to variant problem (Lean). Contribution type: AI standalone.

DeepMind prover agent
LFCR
Partial resultCombinatoricsErdős #872

Erdős problem #872

Partial result. Contribution type: AI standalone.

GPT-5.2 Pro
LFCR
Partial resultCombinatoricsErdős #1082

Erdős problem #1082

Counterexample to one part (Lean). Contribution type: AI alongside literature.

DeepMind prover agent
LFCR
Partial resultCombinatoricsErdős #513

Erdős problem #513

Numerical certificate. Contribution type: Computation.

GPT-5.2 Pro
LFCR