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.

January 2026 40

Literature foundCombinatoricsErdős #543

Erdős problem #543

GPT-5.2 Pro (2026). Contribution type: Rewriting.

GPT-5.2 Thinking
LFCR
Error foundCombinatoricsErdős #963

Erdős problem #963

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

Gemini 3 Pro
LFCR
FormalizationCombinatoricsErdős #728

Erdős problem #728

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1022

Erdős problem #1022

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #862

Erdős problem #862

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
New proofCombinatoricsErdős #543

Erdős problem #543

Full solution. Contribution type: AI alongside literature.

GPT-5.2 Pro
LFCR
Literature foundCombinatoricsErdős #1084

Erdős problem #1084

Partial results found. Contribution type: Literature search.

GPT
LFCR
New proofCombinatoricsErdős #1047

Erdős problem #1047

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

Aristotle
LFCR
Literature foundCombinatoricsErdős #1021

Erdős problem #1021

Full solution (which was previously noted) found. Contribution type: Literature search.

GPT
LFCR
Partial resultCombinatoricsErdős #788

Erdős problem #788

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

GPT-5.2 Pro
LFCR
FormalizationCombinatoricsErdős #788

Erdős problem #788

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Partial resultCombinatoricsErdős #342

Erdős problem #342

Partial result. Contribution type: AI collaborating with humans.

GPT-5.2 Pro · GPT-5.4 Pro · Przemek Chojecki
LFCR
FormalizationCombinatoricsErdős #275

Erdős problem #275

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1036

Erdős problem #1036

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #847

Erdős problem #847

Full solution found. Contribution type: Literature search.

GPT-5.2 Pro
LFCR
Partial resultCombinatoricsErdős #684

Erdős problem #684

Partial result. Contribution type: AI collaborating with humans.

GPT-5.2 Thinking · Quanyu Tang
LFCR
Partial resultCombinatoricsErdős #42

Erdős problem #42

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

Codex · GPT-5.2 · GPT-5.2 Pro
LFCR
FormalizationCombinatoricsErdős #281

Erdős problem #281

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Gemini 3 Flash
LFCR
Literature foundCombinatoricsErdős #1105

Erdős problem #1105

Partial results found. Contribution type: Literature search.

ChatGPT Deep research
LFCR
FormalizationCombinatoricsErdős #1037

Erdős problem #1037

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1028

Erdős problem #1028

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1007

Erdős problem #1007

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
New proofCombinatoricsErdős #1007

Erdős problem #1007

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

Aristotle
LFCR
Error foundCombinatoricsErdős #888

Erdős problem #888

Incorrect proof found. Contribution type: AI standalone.

Claude Opus 4.5 · Gemini 3 Pro · GPT-5.2 Thinking
LFCR
Error foundCombinatoricsErdős #616

Erdős problem #616

Incorrect proof found. Contribution type: AI standalone.

Claude Sonnet 4.5 · Gemini 3 Pro · GPT-5.2 Pro
LFCR
Error foundCombinatoricsErdős #233

Erdős problem #233

Incorrect (conditional) proof found. Contribution type: AI standalone.

GPT-5.2 Pro
LFCR
Literature foundCombinatoricsErdős #652

Erdős problem #652

Full solution by applying literature results. Contribution type: Literature search.

GPT-5.2 Pro
LFCR
Literature foundCombinatoricsErdős #591

Erdős problem #591

Full solution found. Contribution type: Literature search.

ChatGPT Deep research
LFCR
Literature foundCombinatoricsErdős #281

Erdős problem #281

GPT-5.2 Pro (2026). Contribution type: Rewriting.

Gemini 3 Pro · GPT-5.2 Pro
LFCR
New proofCombinatoricsErdős #281

Erdős problem #281

Full solution. Contribution type: AI alongside literature.

GPT-5.2 Pro
LFCR
Literature foundCombinatoricsErdős #1130

Erdős problem #1130

Full solution found. Contribution type: Literature search.

GPT-5.2 Pro
LFCR
Literature foundCombinatoricsErdős #1129

Erdős problem #1129

Full solution found. Contribution type: Literature search.

GPT-5.2 Pro
LFCR
FormalizationCombinatoricsErdős #1008

Erdős problem #1008

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #698

Erdős problem #698

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #94

Erdős problem #94

Formalization of an existing proof. Contribution type: Formalization.

Codex · GPT-5.2 Thinking; Seed Prover
LFCR
FormalizationCombinatoricsErdős #659

Erdős problem #659

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #575

Erdős problem #575

Paper identifying a misstatement to the problem found. Contribution type: Literature search.

GPT
LFCR
FormalizationCombinatoricsErdős #290

Erdős problem #290

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
New proofCombinatoricsErdős #224

Erdős problem #224

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

Codex · GPT-5.2 Thinking
LFCR