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.

September 2026 1

FormalizationNumber theory

Fermat's Last Theorem — new formalization

A new AI-assisted end-to-end Lean development is reported in September, formalizing an already proved theorem.

Claude · Tianyi Peng
LFCR

June 2026 13

FormalizationCombinatoricsErdős #512

Erdős problem #512

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #464

Erdős problem #464

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #716

Erdős problem #716

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1095

Erdős problem #1095

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #441

Erdős problem #441

Formalization of an existing proof. Contribution type: Formalization.

AxiomProver
LFCR
FormalizationCombinatoricsErdős #403

Erdős problem #403

Formalization of an existing proof. Contribution type: Formalization.

AxiomProver
LFCR
FormalizationCombinatoricsErdős #353

Erdős problem #353

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #328

Erdős problem #328

Formalization of an existing proof. Contribution type: Formalization.

AxiomProver
LFCR
FormalizationCombinatoricsErdős #209

Erdős problem #209

Formalization of an existing proof. Contribution type: Formalization.

AxiomProver
LFCR
FormalizationCombinatoricsErdős #1134

Erdős problem #1134

Formalization of an existing proof. Contribution type: Formalization.

AxiomProver
LFCR
FormalizationCombinatoricsErdős #986

Erdős problem #986

Formalization of an existing proof. Contribution type: Formalization.

Trellis
LFCR
FormalizationCombinatoricsErdős #165

Erdős problem #165

Formalization of an existing proof. Contribution type: Formalization.

Trellis
LFCR
FormalizationCombinatoricsErdős #927

Erdős problem #927

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR

May 2026 24

FormalizationCombinatoricsErdős #71

Erdős problem #71

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Claude Opus 4.7 · GPT-5.5
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
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
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
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
FormalizationCombinatoricsErdős #351

Erdős problem #351

Formalization of an existing proof. Contribution type: Formalization.

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

Erdős problem #283

Formalization of an existing proof. Contribution type: Formalization.

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

Erdős problem #1151

Formalization of an existing proof. Contribution type: Formalization.

Codex · GPT
LFCR
FormalizationCombinatoricsErdős #425

Erdős problem #425

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT
LFCR
FormalizationCombinatoricsErdős #330

Erdős problem #330

Formalization of an existing proof. Contribution type: Formalization.

Codex · GPT-5.5 Pro
LFCR
FormalizationCombinatoricsErdős #750

Erdős problem #750

Formalization of an existing proof. Contribution type: Formalization.

Claude Code · Claude Opus 4.7 · GPT-5.5 Pro
LFCR
FormalizationCombinatoricsErdős #164

Erdős problem #164

Formalization of an existing proof. Contribution type: Formalization.

Codex
LFCR
FormalizationCombinatoricsErdős #1138

Erdős problem #1138

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #694

Erdős problem #694

Formalization of an existing proof. Contribution type: Formalization.

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

Erdős problem #639

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #38

Erdős problem #38

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR

April 2026 2

FormalizationCombinatoricsErdős #206

Erdős problem #206

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #1044

Erdős problem #1044

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR