---
id: 20260924-T0-04
title: "FrontierMath Erdos：68道未解数学猜想，AI用Lean证明器来挑战"
title_en: "FrontierMath Erdos Benchmark Tasks AI with 68 Open Math Conjectures in Lean"
url: https://ai.daily.yangsir.net/daily/20260924-T0-04
issue_date: 2026-09-24
publish_date: 2026-09-23T04:00:00.000Z
category: research
source_name: "arXiv cs.CL (NLP)"
source_url: https://arxiv.org/abs/2609.25050
---

# FrontierMath Erdos：68道未解数学猜想，AI用Lean证明器来挑战

研究者发布FrontierMath Erdos（FME）基准，包含68道截至2026年8月仍未解决的Erdos数学猜想问题。AI系统需要在证明助手Lean中对这些猜想进行证明或证伪。该基准旨在测试AI在形式化数学推理上的能力上限，68道题目均来自未解猜想，难度远超常规数学基准。

## English Version

**FrontierMath Erdos Benchmark Tasks AI with 68 Open Math Conjectures in Lean**

Researchers introduced FrontierMath Erdos (FME), a benchmark of 68 Erdos conjectures that remained open as of August 2026. To solve each task, AI systems must prove or disprove the conjecture using the Lean proof assistant. The benchmark is designed to push the limits of formal mathematical reasoning in AI, with all 68 problems drawn from unsolved conjectures, making it substantially harder than conventional math benchmarks.

---

**来源**：[arXiv cs.CL (NLP)](https://arxiv.org/abs/2609.25050)

**详情页**：https://ai.daily.yangsir.net/daily/20260924-T0-04

---

*智语观潮 · Daily — https://ai.daily.yangsir.net/llms.txt*