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.

June 2026 8

FormalizationCombinatoricsErdős #986

Erdős problem #986

Formalization of an existing proof. Contribution type: Formalization.

Trellis
LFCR
Partial resultCombinatoricsErdős #539

Erdős problem #539

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

Codex · GPT-5.5 · ProofCouncil
LFCR
FormalizationCombinatoricsErdős #165

Erdős problem #165

Formalization of an existing proof. Contribution type: Formalization.

Trellis
LFCR
New proofCombinatoricsErdős #619

Erdős problem #619

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

Claude Fable 5 · Codex · GPT-5.5
LFCR
FormalizationCombinatoricsErdős #927

Erdős problem #927

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Candidate solutionCombinatoricsErdős #623

Erdős problem #623

Candidate full solution. Contribution type: AI collaborating with humans.

GPT-5.5 Pro · Sungchul Lee
LFCR
Candidate solutionCombinatoricsErdős #52

Erdős problem #52

Candidate solution to variant problem. Contribution type: AI collaborating with humans.

GPT-5.5 · Boris Alexeev
LFCR
Partial resultCombinatoricsErdős #52

Erdős problem #52

Solution to variant problem. Contribution type: AI standalone.

Claude Mythos
LFCR

May 2026 32

Candidate solutionCombinatoricsErdős #501

Erdős problem #501

Candidate conditional partial result (conditional solution to first part). Contribution type: AI collaborating with humans.

GPT-5.5 Pro · Sungchul Lee
LFCR
Partial resultCombinatoricsErdős #352

Erdős problem #352

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

GPT-5.4 Pro · GPT-5.5 Pro · Aleksandar Bulj · Vjekoslav Kovač
LFCR
Partial resultCombinatoricsErdős #52

Erdős problem #52

Solution to variant problem. Contribution type: AI collaborating with humans.

GPT-5.5 Pro · Thomas Bloom, Will Sawin, Carl Schildkraut +1
LFCR
Partial resultCombinatoricsErdős #52

Erdős problem #52

Improved bound to variant problem. Contribution type: AI collaborating with humans.

GPT-5.5 · Ingo Althöfer
LFCR
New proofCombinatoricsErdős #986

Erdős problem #986

Full solution. Contribution type: AI collaborating with humans.

Claude · OpenAI internal model · Domagoj Bradač
LFCR
Partial resultCombinatoricsErdős #503

Erdős problem #503

Partial result. Contribution type: AI collaborating with humans.

GPT-5.5 Pro · Przemek Chojecki · Junnosuke Koizumi · RealBelgian
LFCR
FormalizationCombinatoricsErdős #71

Erdős problem #71

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.7 · GPT-5.5
LFCR
New proofCombinatoricsErdős #326

Erdős problem #326

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

Aristotle · Codex · GPT-5.5 · Aron Bhalla
LFCR
Partial resultCombinatoricsErdős #1148

Erdős problem #1148

Solution to stronger problem. Contribution type: AI collaborating with humans.

GPT-5.5 Pro · Ingo Althöfer · Przemek Chojecki
LFCR
FormalizationCombinatoricsErdős #603

Erdős problem #603

Formalization of an existing proof. Contribution type: Formalization.

Codex · GPT-5.5
LFCR
FormalizationCombinatoricsErdős #490

Erdős problem #490

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT-5.5 Pro
LFCR
FormalizationCombinatoricsErdős #765

Erdős problem #765

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Partial resultCombinatoricsErdős #345

Erdős problem #345

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

Aristotle · GPT · Wouter van Doorn
LFCR
Candidate solutionCombinatoricsErdős #819

Erdős problem #819

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

GPT-5.5 · Rethlas · Yu Leon Liu
LFCR
FormalizationCombinatoricsErdős #1039

Erdős problem #1039

Formalization of an existing proof. Contribution type: Formalization.

Codex · GPT-5.5
LFCR
FormalizationCombinatoricsErdős #202

Erdős problem #202

Formalization of an existing proof. Contribution type: Formalization.

Unspecified
LFCR
FormalizationCombinatoricsErdős #1190

Erdős problem #1190

Formalization of an existing proof. Contribution type: Formalization.

Unspecified
LFCR
Candidate solutionCombinatoricsErdős #327

Erdős problem #327

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

GPT-5.5 · Rethlas · Yu Leon Liu
LFCR
FormalizationCombinatoricsErdős #1187

Erdős problem #1187

Formalization of an existing proof. Contribution type: Formalization.

Codex · GPT-5.5
LFCR
FormalizationCombinatoricsErdős #42

Erdős problem #42

Formalization of an existing proof. Contribution type: Formalization.

Codex · GPT-5.5 Pro
LFCR
Partial resultCombinatoricsErdős #263

Erdős problem #263

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

Aristotle · Claude Opus 4.7 · GPT-5.5 Pro
LFCR
FormalizationCombinatoricsErdős #231

Erdős problem #231

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #192

Erdős problem #192

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #798

Erdős problem #798

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
New proofCombinatoricsErdős #690

Erdős problem #690

Full solution. Contribution type: AI collaborating with humans.

Multiscalar Fields System · Davide Crapis · Shouqiao Wang
LFCR