Benchmark definition

FrontierMath Erdős

2026-09

ActiveEstablishedCommon useFRONTIERMATH_ERDOS

A 68-conjecture benchmark of significant open Erdős problems formalized in Lean.

Applicability does not mean evaluated; benchmark result/model score data is outside this UI contract.

Compare with others

About

Description: FrontierMath Erdős contains 68 Lean conjectures covering 65 Erdős problems that were open as of August 2026. Models must produce complete Lean proofs or disproofs under a fixed evaluation budget.
What it measures: Research-level mathematical theorem proving in Lean on significant open problems.
What it does not measure: It is not representative of all mathematics and is vulnerable to future contamination as solutions become public.
Comparison guidance: Not published
Intended difficulty: Not published

Not recorded for this benchmark: why it matters, motivation, gap addressed.

Classification

Categories: Formal reasoningResearch mathematicsMathematics
Domains: Research mathematicsMathematics
Evaluation style: AgenticExecutable test based

Structure

One undivided item set. No components or scenarios recorded.

Tasks

None recorded

Metrics

What a result on this benchmark would be reported as. ctxdex does not carry results.

Metric	Role	Direction	Unit
Formal Proof Acceptance	Primary	Higher is better	Percent

Methodology

None recorded

Evaluation environment

What the benchmark's harness provides and allows. These are properties of the environment, not model requirements, and applicability does not test for them.

Interaction: None. Static prompts and answers.
Evaluation style: Agentic, Executable test based
Environment summary: Not published

Model requirements

Required conditions decide applicability. Relevant ones describe what the benchmark exercises and decide nothing.

Required · decides applicability

Whole benchmark

Text (input)Text (output)Formal theorem proving

Relevant · informational

Code generationComplex reasoningExplicit reasoningCoding modelsReasoning models

CTXDEX models

0 of the 58 active, preview, experimental models meet this benchmark’s recorded requirements, at some scope. Applicable means the requirements are met, not that the model was evaluated.

View the 58 not recorded →

Applicable · full: 0
Applicable · components: 0
Applicable · scenarios: 0
Conditionally applicable: 0
Not recorded: 58

Counted over 58 models in the default lifecycle scope (active, preview, experimental).

Applicability/relevance ordering only; never a performance ranking.

Scale

68
Conjecture
Total · Exact
65
Erdos problem
Distinct source problems · Exact

Data and access

Dataset: Open
Evaluation code: Open source
Unknown: Leaderboard, Peer review, Maintenance

Coverage

Languages, regions: None recorded
Coverage summary: Not published

Limitations

None recorded

Lineage

Family: FamilyFrontierMath
Related: None recorded
Other definitions in family: FrontierMath Tier 4 v2 (2026-06-12) ActiveFrontierMath Tier 4 v1 (old) SupersededFrontierMath Tiers 1–3 v2 (2026-06-12) ActiveFrontierMath Tiers 1–3 v1 (old) SupersededFrontierMath Tiers 1–4 Active
Changes: None recorded

Sources

FrontierMath Erdős benchmark page ↗Official website · Benchmark official
FrontierMath Erdős announcement ↗Official website · Benchmark official

Freshness

Content version: 1.0
Last reviewed: 2026-09-22
Refresh model: Periodic
Time sensitivity: Medium
Benchmark data: c40cccac878af5d0

13 contract fields are empty for every benchmark in this release and are not shown: applicability groups, conditional requirements, feature requirements, model relevance domains, required capabilities, openness summary, reference artifacts, interaction protocols, tool protocols, benchmark last major refresh at, short name, target expertise level, target population.