2026年开年以来，AI 以摧枯拉朽的速度完整解决了至少10个Erdős问题，如果把新解也考虑在内，那就是19个，数学科研的珍妮纺纱机已经出现了。

详情：

根据著名数学家陶哲轩维护的名叫 AI contributions to Erdős problems 的 wiki （最后一次更新在3月28日）统计，2026年1月–3月底，AI 在 Erdős 问题上的”完整解决”按四类分布： • 1(a) AI 自主首解（文献无前作）：3 • 1(b) AI 解出，事后才发现已有文献：9 • 1(c) 已解问题的新证明：9 • 1(d) 人-AI 协作：6

共 27 条记录（跨类去重后26，#659 在 1(b) 和 1(d) 各出现一次）

不考虑事后发现已有文献的一类，再考虑OpenAI 在5月20日公布的著名硬骨头 #90 的突破等进展还未更新，AI 到2026年5月24日至少也已经完整解决了19个Erdős问题，生产队的驴都没这么勤。

teorth/erdosproblems

Source: https://github.com/teorth/erdosproblems

Erdős problem database

Browse the interactive table - Sort, filter, and search all the problems in the database

A community database for the problems on the erdosproblems.com site. We are particularly seeking community contributions regarding the integer sequences associated with these problems, and linking them to the OEIS.

The table below is auto-generated from the YAML file data/problems.yaml, which is the “ground truth” for this data as far as this repository is concerned.

• To propose changes, open a PR editing data/problems.yaml.
• See CONTRIBUTING.md for guidelines and field definitions.

For further discussion of this project, see this blog post (from Sep 1, 2025).

Several of the problems have received assistance from various AI tools. A list of such assistance can be found here.

Progress

Table

There are 1217 problems in total, of which

• 106 are attached to a monetary prize.
• 323 have been proved.
  • 107 of these proofs have been formalized in Lean.
• 132 have been disproved.
  • 56 of these disproofs have been formalized in Lean.
• 82 have been otherwise solved.
  • 20 of these solutions have been formalized in Lean.
• 3 appear to be open, but cannot be proven from the axioms of ZFC. (not provable)
• 4 appear to be open, but cannot be disproven from the axioms of ZFC. (not disprovable)
• 3 are known to be independent of the ZFC axioms of mathematics. (independent)
• 9 appear to be open, but have been reduced to a finite computation. (decidable)
• 27 appear to be open, but can be disproven by a finite computation if false. (falsifiable)
• 7 appear to be open, but can be proven by a finite computation if true. (verifiable)
• 627 appear to be completely open.
• 7 have ambiguous statements.
• 0 have a literature review requested.
• 425 have their statements formalized in Lean in the Formal Conjectures Repository.
• 311 have been linked to 385 distinct OEIS sequences, with a total of 462 links created.
  • 78 of these OEIS sequences were added since the creation of this database (A387000 onwards).
• 326 are potentially related to an OEIS sequence not already listed.
  • 278 of these problems are not currently linked to any existing OEIS sequence.
• 0 have a related sequence currently being submitted to the OEIS.
• 1 have a related sequence whose generation is currently in progress.