Machine-checked mathematics
Maths
Eight open problems posed by Erdős, worked in Lean. Everything on these pages is generated from the public Lean repository: the problems, the checked results with their exact boundaries, the papers, and the graph that connects them. All eight problems remain open.
Each problem page names what is proved, under which hypotheses, and what is not. Every object links to its source on GitHub.
- 8 problems
- 13 papers
- 14 repository documents
- 1,292 objects in the universe
- 3,246 connections
The universe
One corpus, three overlays.
The Lean source is the universe. Papers, the Comparator, and Palomar are overlays that explain, replay, or review parts of it.
The interactive map needs JavaScript. Every object on it is listed as text on the universe page.
- Problems
- Checked claims
- Papers
- Documents
- Verification
Papers explain, Comparator replays selected exact interfaces, and Palomar may review a prepared unit. None widens Lean's proposition or records peer review or an accepted outcome unless its own source says so.
The problems
Eight problems, all of them open.
Each dossier states the question, what the Lean corpus proves about it, and exactly what remains unproved.
- #68 The factorial-denominator series Is the series sum_{n >= 2} 1/(n! - 1) irrational?
- #243 Reciprocal-tail rigidity near the Sylvester recurrence Under a rapid-growth hypothesis on an integer sequence, does rationality of its reciprocal sum force the sequence to satisfy the Sylvester recurrence eventually?
- #249 The binary totient series Is the binary Lambert series sum phi(n)/2^n irrational?
- #251 The prime-gap dyadic series Is the dyadic series sum p_n/2^n over consecutive primes irrational? Equivalently, is the corresponding consecutive-prime-gap dyadic series irrational?
- #257 Reciprocal sums over infinite exponent supports Is the sum of 1/(2^n-1) over every infinite set of positive exponents irrational?
- #269 Three-prime running least common multiples For a finite set of at least two primes, is the sum of reciprocals of the running least common multiples of the smooth numbers irrational? This library treats the three-prime case.
- #1041 Short connections inside polynomial lemniscates For a monic polynomial whose roots lie in the open unit disc, must two roots be joinable by a curve of length less than two inside the open unit lemniscate?
- #1049 Lambert-type series at rational bases For which rational bases is the corresponding series irrational? The smallest resistant explicit base is three halves.
The papers
Read the mathematics as papers.
Written for a person reading cold, rendered here as pages with native mathematical notation; the PDF and the LaTeX source stay one click away. Papers explain the corpus; they are not the proof authority.
On the problems
The repository, in plain pages
Read the repository without building it.
A curated human interpretability layer over the Lean repository. It excludes agent instructions, machine-heavy atlases, build artifacts, and maintainer workbenches.
These pages are generated from the public Lean repository’s published data layer; nothing here is written by hand. Source generation a18f18bba79573a1, built by tools/meta/dissemination/build_plectis_maths_site.py from the contract in lean/experience/manifest.json. When the repository changes, a redeploy regenerates every page, count, and map above.