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 40

Partial resultCombinatoricsErdős #374

Erdős problem #374

Partial result. Contribution type: AI collaborating with humans.

GPT-5.4 Pro · Terence Tao
LFCR
FormalizationCombinatoricsErdős #150

Erdős problem #150

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
New proofCombinatoricsErdős #125

Erdős problem #125

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

DeepMind prover agent
LFCR
Literature foundCombinatoricsErdős #574

Erdős problem #574

Full solution found. Contribution type: Literature search.

GPT-5.4 Pro
LFCR
FormalizationCombinatoricsErdős #283

Erdős problem #283

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #369

Erdős problem #369

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
New proofCombinatoricsErdős #369

Erdős problem #369

Full solution. Contribution type: AI collaborating with humans.

GPT · Sky Yang
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
FormalizationCombinatoricsErdős #1148

Erdős problem #1148

Formalization of an existing proof. Contribution type: Formalization.

Claude Opus 4.6 · Gemini 3.1 · GPT-5.4 · UlamAI Prover
LFCR
Error foundCombinatoricsErdős #1041

Erdős problem #1041

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

Claude Opus 4.6 · Gemini 3.1 Pro · GPT-5.4 · shtuka
LFCR
FormalizationCombinatoricsErdős #756

Erdős problem #756

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Partial resultCombinatoricsErdős #396

Erdős problem #396

Partial result. Contribution type: AI collaborating with humans.

Claude · Codex · GPT · Malek Zribi
LFCR
FormalizationCombinatoricsErdős #204

Erdős problem #204

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #120

Erdős problem #120

Solution to variant problem found. Contribution type: Literature search.

GPT-5.4 Thinking
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
Error foundCombinatoricsErdős #848

Erdős problem #848

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

Claude Opus 4.6 · GPT-5.4 · Malek Zribi
LFCR
Error foundCombinatoricsErdős #388

Erdős problem #388

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

Claude · Gemini · GPT-5.4 · Malek Zribi
LFCR
FormalizationCombinatoricsErdős #459

Erdős problem #459

Formalization of an existing proof. Contribution type: Formalization.

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

Erdős problem #363

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #1216

Erdős problem #1216

Solution stronger than problem found. Contribution type: Literature search.

ChatGPT Deep research
LFCR
Partial resultCombinatoricsErdős #349

Erdős problem #349

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

GPT-5.2 Thinking
LFCR
Literature foundCombinatoricsErdős #325

Erdős problem #325

Partial results found. Contribution type: Literature search.

ChatGPT Deep research
LFCR
Partial resultCombinatoricsErdős #650

Erdős problem #650

Numerical optimization. Contribution type: Computation.

AlphaEvolve
LFCR
Literature foundCombinatoricsErdős #985

Erdős problem #985

Partial results found. Contribution type: Literature search.

GPT-5.4 Thinking
LFCR
FormalizationCombinatoricsErdős #785

Erdős problem #785

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #650

Erdős problem #650

Full solution found. Contribution type: Literature search.

ChatGPT Deep research
LFCR
FormalizationCombinatoricsErdős #650

Erdős problem #650

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
New proofCombinatoricsErdős #650

Erdős problem #650

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

GPT-5.4 Pro
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
Literature foundCombinatoricsErdős #457

Erdős problem #457

Tao (2026) (extension of problem). Contribution type: Rewriting.

GPT-5.2 Thinking
LFCR
FormalizationCombinatoricsErdős #115

Erdős problem #115

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.6 · Claude Sonnet 4.6 · Gemini 3 Flash · Gemini 3.1 Pro · ulam.ai scaffold with Gemini 3 Flash and Gemini 3.1 Pro
LFCR
New proofCombinatoricsErdős #457

Erdős problem #457

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

Aristotle · GPT-5.2 Pro
LFCR
FormalizationCombinatoricsErdős #214

Erdős problem #214

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR