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 11

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

Erdős problem #756

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #204

Erdős problem #204

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #459

Erdős problem #459

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #363

Erdős problem #363

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #785

Erdős problem #785

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #650

Erdős problem #650

Formalization of an existing proof. Contribution type: Formalization.

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

Erdős problem #214

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR

February 2026 29

FormalizationCombinatoricsErdős #646

Erdős problem #646

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1126

Erdős problem #1126

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #16

Erdős problem #16

Formalization of an existing proof. Contribution type: Formalization.

Antigravity · Gemini 3.1 Pro
LFCR
FormalizationCombinatoricsErdős #434

Erdős problem #434

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.8
LFCR
FormalizationCombinatoricsErdős #433

Erdős problem #433

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.8 · Claude Sonnet 4.6 · Gemini 3 Flash · Gemini 3.1 Pro · Project Numina
LFCR
FormalizationCombinatoricsErdős #199

Erdős problem #199

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1102

Erdős problem #1102

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #93

Erdős problem #93

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.5 · Claude Opus 4.6 · Gemini 3 Flash · Gemini 3 Pro · Numina Lean Agent
LFCR
FormalizationCombinatoricsErdős #368

Erdős problem #368

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #487

Erdős problem #487

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #964

Erdős problem #964

Formalization of an existing proof. Contribution type: Formalization.

Antigravity · Aristotle · Gemini
LFCR
FormalizationCombinatoricsErdős #447

Erdős problem #447

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1023

Erdős problem #1023

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #762

Erdős problem #762

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.7 · GPT
LFCR
FormalizationCombinatoricsErdős #618

Erdős problem #618

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #649

Erdős problem #649

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT
LFCR
FormalizationCombinatoricsErdős #134

Erdős problem #134

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #666

Erdős problem #666

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #537

Erdős problem #537

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #154

Erdős problem #154

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT
LFCR
FormalizationCombinatoricsErdős #794

Erdős problem #794

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #582

Erdős problem #582

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #34

Erdős problem #34

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #648

Erdős problem #648

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #497

Erdős problem #497

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #443

Erdős problem #443

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #435

Erdős problem #435

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #947

Erdős problem #947

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT
LFCR
FormalizationCombinatoricsErdős #505

Erdős problem #505

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR