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 24

Partial resultCombinatoricsErdős #868

Erdős problem #868

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

GPT-5.2 multi-agent system
LFCR
New proofCombinatoricsErdős #659

Erdős problem #659

Full solution. Contribution type: AI collaborating with humans.

Gemini 3 · Benjamin Grayzel
LFCR
Literature foundCombinatoricsErdős #659

Erdős problem #659

Partial results, upgradeable to full solution, found. Contribution type: Literature search.

Gemini Deep Research
LFCR
Partial resultCombinatoricsErdős #460

Erdős problem #460

Reduction to a simpler problem. Contribution type: AI collaborating with humans.

GPT-5.2 · Przemek Chojecki
LFCR
Partial resultCombinatoricsErdős #679

Erdős problem #679

Improved proof by reducing dependence on prime number theorem. Contribution type: AI building on literature.

Aristotle
LFCR
Error foundCombinatoricsErdős #51

Erdős problem #51

Incorrect proof found. Contribution type: AI standalone.

ChatGPT free version
LFCR
Literature foundCombinatoricsErdős #729

Erdős problem #729

Related results found. Contribution type: Literature search.

ChatGPT Deep research
LFCR
New proofCombinatoricsErdős #401

Erdős problem #401

Full solution (Lean); solution to variant problem. Contribution type: AI collaborating with humans.

Aristotle · GPT-5.2 Pro · Boris Alexeev, Kevin Barreto, Liam Price +1
LFCR
New proofCombinatoricsErdős #397

Erdős problem #397

Full solution (Lean). Contribution type: AI alongside literature.

Aristotle · GPT-5.2 Pro
LFCR
Literature foundCombinatoricsErdős #397

Erdős problem #397

Full solution found. Contribution type: Literature search.

ChatGPT Deep research
LFCR
New proofCombinatoricsErdős #205

Erdős problem #205

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

Aristotle · GPT-5.2 Thinking
LFCR
FormalizationCombinatoricsErdős #845

Erdős problem #845

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
New proofCombinatoricsErdős #729

Erdős problem #729

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

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

Erdős problem #949

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

AlphaProof
LFCR
FormalizationCombinatoricsErdős #678

Erdős problem #678

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
Literature foundCombinatoricsErdős #672

Erdős problem #672

Partial results found. Contribution type: Literature search.

GPT
LFCR
Partial resultCombinatoricsErdős #477

Erdős problem #477

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

AlphaProof
LFCR
New proofCombinatoricsErdős #728

Erdős problem #728

Full solution (Lean). Contribution type: AI alongside literature.

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

Erdős problem #392

Formalization of an existing proof. Contribution type: Formalization.

Various
LFCR
Partial resultCombinatoricsErdős #871

Erdős problem #871

Existing partial result upgraded to full solution (Lean). Contribution type: AI building on literature.

Claude Opus 4.5 · Gemini 3 Pro
LFCR
Literature foundCombinatoricsErdős #728

Erdős problem #728

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

Aristotle · GPT-5.2 Thinking
LFCR
Error foundCombinatoricsErdős #1044

Erdős problem #1044

Incorrect claim made. Contribution type: AI standalone.

GPT-5.2 Pro
LFCR
Literature foundCombinatoricsErdős #965

Erdős problem #965

Full solution found. Contribution type: Literature search.

GPT
LFCR

December 2025 1

Partial resultCombinatoricsErdős #1038

Erdős problem #1038

Partial result. Contribution type: AI collaborating with humans.

AlphaEvolve · Claude Fable 5 · Codex · GPT-5.2 Thinking · GPT-5.4 Thinking · GPT-5.5 · catsflowers5544, jspier, Junnosuke Koizumi +4
LFCR

November 2025 1

FormalizationCombinatoricsErdős #56

Erdős problem #56

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT
LFCR

October 2025 2

Candidate solutionCombinatoricsErdős #689

Erdős problem #689

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

Codex · GPT-5.2 · GPT-5.5 Pro · Boris Alexeev, Przemek Chojecki, Dogmachine +4
LFCR
New proofCombinatoricsErdős #347

Erdős problem #347

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

Aristotle · Claude Opus · Codex · GPT · Enrique Barschkis, Wouter van Doorn, jbbaehr22 +2
LFCR

August 2025 1

Partial resultCombinatoricsErdős #686

Erdős problem #686

Various partial results. Contribution type: AI collaborating with humans.

AlphaProof · Claude · Gemini Deep Think · GPT-5.2 Thinking · GPT-5.4 Thinking · Seed 2.0 Pro · Adenwalla, Stijn Cambie, Wouter van Doorn +7
LFCR

Date not recorded 2

CounterexampleCombinatorics

Devin graph and spectral-conjecture results

Nine-vertex Brandt counterexample; proofs for WoW 698 and Graffiti 39/40; independent refutations for Graffiti 143/154 with explicit earlier-priority qualification.

LFCR