# Summary statistics

Aggregate counts over [data/problems.yaml](data/problems.yaml) — how many problems are proved, disproved, open, formalized in Lean, linked to the OEIS, and so on.  Back to the [main page and problem table](README.md).

These counts used to appear at the top of the README.  They were moved here on October 6, 2026, so that a visitor arriving at the repository is not shown a tally of solved problems by default.  This is in accordance with the [policy changes announced at erdosproblems.com](https://www.erdosproblems.com/forum/thread/blog:9) on that date, under which that site no longer displays the statuses of problems, nor the count or percentage of problems solved: the problems are meant to be read as open questions worth understanding rather than as a scoreboard.

The figures are still generated, and the per-problem table on the [main page](README.md) still carries each problem's status, so nothing has been withdrawn from the data — only from the front page.  The [progress chart](README.md#progress) was frozen on the same date for the same reason.

**This page is auto-generated** by [scripts/generate_readme.py](scripts/generate_readme.py) from `data/problems.yaml`.  Do not hand-edit between the markers below; any such edits will be overwritten.

<!-- STATS:START -->
There are 1221 problems in total, of which
- [107](https://teorth.github.io/erdosproblems/?prize=yes) are attached to a monetary prize.
- [336](https://teorth.github.io/erdosproblems/?status=proved) have been proved.
  - [183](https://teorth.github.io/erdosproblems/?status=proved&formal=Lean) of these proofs have been formalized in [Lean](https://lean-lang.org/).
- [139](https://teorth.github.io/erdosproblems/?status=disproved) have been disproved.
  - [97](https://teorth.github.io/erdosproblems/?status=disproved&formal=Lean) of these disproofs have been formalized in [Lean](https://lean-lang.org/).
- [101](https://teorth.github.io/erdosproblems/?status=solved) have been otherwise solved.
  - [33](https://teorth.github.io/erdosproblems/?status=solved&formal=Lean) of these solutions have been formalized in [Lean](https://lean-lang.org/).
- [3](https://teorth.github.io/erdosproblems/?status=not+provable) appear to be open, but cannot be proven from the axioms of ZFC. (not provable)
- [6](https://teorth.github.io/erdosproblems/?status=not+disprovable) appear to be open, but cannot be disproven from the axioms of ZFC. (not disprovable)
- [3](https://teorth.github.io/erdosproblems/?status=independent) are known to be independent of the ZFC axioms of mathematics. (independent)
- [8](https://teorth.github.io/erdosproblems/?status=decidable) appear to be open, but have been reduced to a finite computation. (decidable)
- [25](https://teorth.github.io/erdosproblems/?status=falsifiable) appear to be open, but can be disproven by a finite computation if false. (falsifiable)
- [7](https://teorth.github.io/erdosproblems/?status=verifiable) appear to be open, but can be proven by a finite computation if true. (verifiable)
- [593](https://teorth.github.io/erdosproblems/?status=open) appear to be completely open.
- 11 have ambiguous statements.
- 0 have a literature review requested.
- [318](https://teorth.github.io/erdosproblems/?formal=Lean) have a *solution* formalized in [Lean](https://lean-lang.org/).  This need not be a subset of the solved problems above: a formalized solution that has not yet been digested by a human reader keeps its informal status (so can appear as, e.g., "open (Lean)").
- [957](https://teorth.github.io/erdosproblems/?formalized=yes) have their *statements* formalized in [Lean](https://lean-lang.org/) in the [Formal Conjectures Repository](https://github.com/google-deepmind/formal-conjectures).
- [358](https://teorth.github.io/erdosproblems/?oeis=linked) have been linked to 474 distinct [OEIS](https://oeis.org/) sequences, with a total of 558 links created.
  - 107 of these OEIS sequences were added since the creation of this database (A387000 onwards).
- [310](https://teorth.github.io/erdosproblems/?oeis=possible) are potentially related to an [OEIS](https://oeis.org/) sequence not already listed.
  - 235 of these problems are not currently linked to any existing [OEIS](https://oeis.org/) sequence.
- 0 have a related sequence currently being submitted to the [OEIS](https://oeis.org/).
- [1](https://teorth.github.io/erdosproblems/?oeis=inprogress) have a related sequence whose generation is currently in progress.
<!-- STATS:END -->