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.

February 2026 4

Literature foundCombinatoricsErdős #333

Erdős problem #333

Full solution found. Contribution type: Literature search.

Aletheia
LFCR
Literature foundCombinatoricsErdős #1105

Erdős problem #1105

Full solution found; 🔴 Gave some wrong references. Contribution type: Literature search.

Aletheia
LFCR
New proofCombinatoricsErdős #1089

Erdős problem #1089

Full solution found. Contribution type: AI alongside literature.

Aletheia
LFCR
Partial resultCombinatoricsErdős #1040

Erdős problem #1040

Solution to one part of problem; 🔴 incorrect solution to other part. Contribution type: AI standalone.

Aletheia
LFCR

January 2026 36

Literature foundCombinatoricsErdős #971

Erdős problem #971

Partial results found. Contribution type: Literature search.

Claude
LFCR
FormalizationCombinatoricsErdős #453

Erdős problem #453

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #419

Erdős problem #419

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #331

Erdős problem #331

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #315

Erdős problem #315

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #221

Erdős problem #221

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #1123

Erdős problem #1123

Full solution found. Contribution type: Literature search.

Gemini Deep Research
LFCR
Partial resultCombinatoricsErdős #635

Erdős problem #635

Solution to one part of problem (Lean). Contribution type: AI alongside literature.

Aristotle · GPT-5.2 Pro
LFCR
Partial resultCombinatoricsErdős #524

Erdős problem #524

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

Gemini · GPT-5.2 · Grok
LFCR
FormalizationCombinatoricsErdős #355

Erdős problem #355

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Gemini 3
LFCR
FormalizationCombinatoricsErdős #429

Erdős problem #429

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1071

Erdős problem #1071

Formalization of an existing proof. Contribution type: Formalization.

Aleph Prover · Aristotle · GPT
LFCR
New proofCombinatoricsErdős #1051

Erdős problem #1051

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

Aletheia
LFCR
Partial resultCombinatoricsErdős #951

Erdős problem #951

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

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

Erdős problem #951

New solution to variant problem. Contribution type: AI building on literature.

AlphaEvolve
LFCR
FormalizationCombinatoricsErdős #898

Erdős problem #898

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Gemini 3 Flash
LFCR
FormalizationCombinatoricsErdős #848

Erdős problem #848

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude · GPT-5.2
LFCR
Error foundCombinatoricsErdős #647

Erdős problem #647

Incorrect proof found. Contribution type: AI standalone.

ChatGPT Deep research · DeepSeek DeepThink · Gemini
LFCR
Partial resultCombinatoricsErdős #218

Erdős problem #218

Conditional solution. Contribution type: AI alongside literature.

GPT
LFCR
FormalizationCombinatoricsErdős #1067

Erdős problem #1067

Formalization of an existing proof. Contribution type: Formalization.

Aleph Prover · Aristotle
LFCR
Partial resultCombinatoricsErdős #1048

Erdős problem #1048

Proof found (Lean), which is a specific case of Pommerenke. Contribution type: AI building on literature.

Aristotle
LFCR
Partial resultCombinatoricsErdős #951

Erdős problem #951

Solution to variant problem. Contribution type: AI standalone.

GPT-5.2 Pro
LFCR
FormalizationCombinatoricsErdős #751

Erdős problem #751

Formalization of an existing proof. Contribution type: Formalization.

GPT-5.2-Codex · GPT-5.2 Thinking
LFCR
FormalizationCombinatoricsErdős #498

Erdős problem #498

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus · Gemini Flash · Gemini Pro
LFCR
FormalizationCombinatoricsErdős #1048

Erdős problem #1048

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #705

Erdős problem #705

Full solution found. Contribution type: Literature search.

GPT
LFCR
Literature foundCombinatoricsErdős #533

Erdős problem #533

Full solution found. Contribution type: Literature search.

GPT
LFCR
Literature foundCombinatoricsErdős #1147

Erdős problem #1147

Full solution found. Contribution type: Literature search.

GPT-5.2 Thinking
LFCR
Candidate solutionCombinatoricsErdős #1139

Erdős problem #1139

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

GPT-5.2 Pro · GPT-5.5 Pro · Przemek Chojecki, gavinsherry, Liam Price +1
LFCR
Partial resultCombinatoricsErdős #1141

Erdős problem #1141

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

GPT-5.2 Pro · GPT-5.2 Thinking · Quanyu Tang
LFCR
Literature foundCombinatoricsErdős #783

Erdős problem #783

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

GPT-5.2 Thinking
LFCR
Literature foundCombinatoricsErdős #1161

Erdős problem #1161

Full solution found. Contribution type: Literature search.

GPT-5.2 Thinking
LFCR
Literature foundCombinatoricsErdős #1154

Erdős problem #1154

Partial results found. Contribution type: Literature search.

GPT-5.2 Thinking
LFCR
New proofCombinatoricsErdős #1148

Erdős problem #1148

Full solution. Contribution type: AI collaborating with humans.

Gemini 3 Pro · Gemini 3.1 Pro · GPT-5.2 Pro · GPT-5.2 Thinking · GPT-5.4 Pro · Ingo Althöfer · Przemek Chojecki · Wouter van Doorn
LFCR
Error foundCombinatoricsErdős #11

Erdős problem #11

Incorrect claim made. Contribution type: AI standalone.

Aristotle · GPT
LFCR
Partial resultCombinatoricsErdős #783

Erdős problem #783

Partial result. Contribution type: AI standalone.

GPT-5.2
LFCR