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 2

FormalizationCombinatoricsErdős #502

Erdős problem #502

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #399

Erdős problem #399

Formalization of an existing proof. Contribution type: Formalization.

Codex
LFCR

January 2026 32

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

Erdős problem #1067

Formalization of an existing proof. Contribution type: Formalization.

Aleph Prover · Aristotle
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
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
FormalizationCombinatoricsErdős #788

Erdős problem #788

Formalization of an existing proof. Contribution type: Formalization.

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

Erdős problem #281

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · Gemini 3 Flash
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
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
FormalizationCombinatoricsErdős #290

Erdős problem #290

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #845

Erdős problem #845

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #678

Erdős problem #678

Formalization of an existing proof. Contribution type: Formalization.

Aristotle
LFCR
FormalizationCombinatoricsErdős #392

Erdős problem #392

Formalization of an existing proof. Contribution type: Formalization.

Various
LFCR

November 2025 1

FormalizationCombinatoricsErdős #56

Erdős problem #56

Formalization of an existing proof. Contribution type: Formalization.

Aristotle · GPT
LFCR