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.

March 2026 1

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 39

FormalizationCombinatoricsErdős #646

Erdős problem #646

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #392

Erdős problem #392

Tao (2026). Contribution type: Rewriting.

GPT-5.2 Thinking
LFCR
FormalizationCombinatoricsErdős #1126

Erdős problem #1126

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Partial resultCombinatoricsErdős #1090

Erdős problem #1090

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

Aristotle · Gemini 3 Flash
LFCR
New proofCombinatoricsErdős #966

Erdős problem #966

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

Aristotle
LFCR
Literature foundCombinatoricsErdős #846

Erdős problem #846

DeepMind prover agent (2026). Contribution type: Rewriting.

GPT-5.2 Thinking
LFCR
Literature foundCombinatoricsErdős #306

Erdős problem #306

Partial results found. Contribution type: Literature search.

GPT-5.2 Thinking
LFCR
FormalizationCombinatoricsErdős #16

Erdős problem #16

Formalization of an existing proof. Contribution type: Formalization.

Antigravity · Gemini 3.1 Pro
LFCR
FormalizationCombinatoricsErdős #434

Erdős problem #434

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.8
LFCR
FormalizationCombinatoricsErdős #433

Erdős problem #433

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.8 · Claude Sonnet 4.6 · Gemini 3 Flash · Gemini 3.1 Pro · Project Numina
LFCR
FormalizationCombinatoricsErdős #199

Erdős problem #199

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1102

Erdős problem #1102

Formalization of an existing proof. Contribution type: Formalization.

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
Literature foundCombinatoricsErdős #783

Erdős problem #783

Tao (2026). Contribution type: Rewriting.

GPT-5.2 Thinking
LFCR
Partial resultCombinatoricsErdős #125

Erdős problem #125

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

DeepMind prover agent
LFCR
Literature foundCombinatoricsErdős #214

Erdős problem #214

Partial results found. Contribution type: Literature search.

ChatGPT Deep research · Gemini Deep Research
LFCR
FormalizationCombinatoricsErdős #93

Erdős problem #93

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.5 · Claude Opus 4.6 · Gemini 3 Flash · Gemini 3 Pro · Numina Lean Agent
LFCR
FormalizationCombinatoricsErdős #368

Erdős problem #368

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Partial resultCombinatoricsErdős #872

Erdős problem #872

Partial result. Contribution type: AI standalone.

GPT-5.2 Pro
LFCR
FormalizationCombinatoricsErdős #487

Erdős problem #487

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #964

Erdős problem #964

Formalization of an existing proof. Contribution type: Formalization.

Antigravity · Aristotle · Gemini
LFCR
Partial resultCombinatoricsErdős #1082

Erdős problem #1082

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

DeepMind prover agent
LFCR
Error foundCombinatoricsErdős #358

Erdős problem #358

Argument with major gaps made. Contribution type: AI collaborating with humans.

GPT-5.2 Thinking · Nat Sothanaphan
LFCR
Partial resultCombinatoricsErdős #513

Erdős problem #513

Numerical certificate. Contribution type: Computation.

GPT-5.2 Pro
LFCR
Partial resultCombinatoricsErdős #776

Erdős problem #776

Partial result. Contribution type: AI collaborating with humans.

GPT-5.2 Thinking · Yixin He · Quanyu Tang
LFCR
Error foundCombinatoricsErdős #358

Erdős problem #358

Argument with major gaps made. Contribution type: AI standalone.

GPT-5.2 Pro
LFCR
FormalizationCombinatoricsErdős #447

Erdős problem #447

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1023

Erdős problem #1023

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #762

Erdős problem #762

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.7 · GPT
LFCR
FormalizationCombinatoricsErdős #618

Erdős problem #618

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #649

Erdős problem #649

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT
LFCR
FormalizationCombinatoricsErdős #134

Erdős problem #134

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #666

Erdős problem #666

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #537

Erdős problem #537

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #154

Erdős problem #154

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT
LFCR
Literature foundCombinatoricsErdős #851

Erdős problem #851

Confused with another problem; 🟡 Partial results found. Contribution type: Literature search.

ChatGPT Deep research · Claude · Gemini Deep Research
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
FormalizationCombinatoricsErdős #794

Erdős problem #794

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #582

Erdős problem #582

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR