mlsanityData to 14 Oct 2026

FrontierMath ErdHos

arXiv 2609.25050 ↗First posted 6 Sep 2026cs.CL cs.AIcited by 0

Not on the map. Why?

Abstract (arXiv)

We introduce FrontierMath ErdHos (FME), a benchmark of 68 ErdHos problems that are open as of August 2026. To solve a task in FME, AI systems must resolve (prove or disprove) one of the 68 conjectures in the proof assistant Lean. Our 68 problems were selected by the second author among 652 open problems on erdosproblems.com for their mathematical interest and difficulty. AIs have recently resolved several open problems in mathematics, but these demonstrations fall short of a systematic study of AI capabilities. FME evaluates every AI model on the same fixed problems, autonomously and under the same budget. We evaluated five AIs with a budget of 300 per problem. One (GPT-6 Astra) scored 3%, and all others scored 0%.

Key facts. No citing papers in the map yet (data through 14 Oct 2026). Builds on 3 of its 20 references that are in the map. First posted on arXiv 6 Sep 2026.

Builds on

3 of 20 references.

References · 3

  1. 2026Advancing Mathematics Research with AI-Driven Formal Proof Searchcited by 23
  2. 2026Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematicscited by 10
  3. 2026OEIS Open: How many conjectures can language models turn into theorems?cited by 2

Built on by

Not cited yet.