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 35

FormalizationCombinatoricsErdős #258

Erdős problem #258

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #268

Erdős problem #268

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
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
FormalizationCombinatoricsErdős #1193

Erdős problem #1193

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Partial resultCombinatoricsErdős #75

Erdős problem #75

Partial result. Contribution type: AI building on literature.

GPT-5.4 Pro
LFCR
Literature foundCombinatoricsErdős #1216

Erdős problem #1216

Related results found. Contribution type: Literature search.

GPT-5.4 Thinking
LFCR
FormalizationCombinatoricsErdős #1141

Erdős problem #1141

Formalization of an existing proof. Contribution type: Formalization.

GPT-5.4 Pro
LFCR
FormalizationCombinatoricsErdős #1125

Erdős problem #1125

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #990

Erdős problem #990

Formalization of an existing proof. Contribution type: Formalization.

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
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
FormalizationCombinatoricsErdős #907

Erdős problem #907

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #905

Erdős problem #905

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT-5.4
LFCR
FormalizationCombinatoricsErdős #867

Erdős problem #867

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
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
FormalizationCombinatoricsErdős #237

Erdős problem #237

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #749

Erdős problem #749

Partial results found. Contribution type: Literature search.

GPT-5.4 Thinking
LFCR
Error foundCombinatoricsErdős #411

Erdős problem #411

Incorrect proof found. Contribution type: AI collaborating with humans.

Claude · hoodieuser
LFCR
New proofCombinatoricsErdős #152

Erdős problem #152

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

DeepMind prover agent
LFCR
FormalizationCombinatoricsErdős #692

Erdős problem #692

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Partial resultCombinatoricsErdős #684

Erdős problem #684

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 Thinking · Nat Sothanaphan
LFCR
FormalizationCombinatoricsErdős #997

Erdős problem #997

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #314

Erdős problem #314

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
New proofCombinatoricsErdős #1202

Erdős problem #1202

Full solution. Contribution type: AI standalone.

GPT-5.4 Pro
LFCR

March 2026 5

New proofCombinatoricsErdős #997

Erdős problem #997

Full solution. Contribution type: AI alongside literature.

OpenAI internal model
LFCR
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
New proofCombinatoricsErdős #380

Erdős problem #380

Full solution. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Terence Tao
LFCR