Will Cook · checkable mathematical research
Plectis writes mathematics with AI and has it machine-checked. The proofs are written in Lean, software that reads every step and rejects the proof if a step does not follow. The work covers eight open problems posed by Erdős, picked for depth rather than for tractability: the corpus and the papers are what a year of pushing today's models at them produced. All eight remain open, and none of this solves one.
Start here
Five results, stated here, the strongest in the corpus. Each gives the question, what was actually proved, what backs it and what is still missing.
Hover or tab to a number for the question, what was checked, and what is still unproved.Open a number for the question, what was checked, and what is still unproved.
#68Exact endpoint
QuestionIs ∑n ≥ 2 1/(n! − 1) irrational?
The original series problem is reduced without loss to an integer event that can be attacked directly.
EvidenceLean checked exact equivalence
Still openForce failures of m dividing the strict successor beyond every cutoff.
Classical factorial radix context; source specific formal synthesis; no priority claim.
#249Canonical reduction
QuestionIs ∑n ≥ 1 φ(n)/2n irrational?
Several competing attack languages collapse to one forced basepoint modular supply with the full quantifier order visible.
EvidenceLean checked exact equivalence
Still openProduce the strict centered gap for every basepoint and every positive odd denominator shape.
Classical radix tails, Euler periodicity and modular arithmetic; no priority claim for the packaging.
The paper covers the problem; this particular equivalence is in the Lean source, not in it.
#251Coordinate change
QuestionIs ∑ pn/2n over the consecutive primes irrational?
Summation by parts keeps the endpoint and identifies the actual infinite obstruction, instead of treating prime irregularity as evidence by itself.
EvidenceLean checked identity, convergence and rational affine equivalence
Still openProve an infinite obstruction for the genuine consecutive prime gap tail.
Exact summation by parts with a direct public antecedent; no new prime gap theorem or novelty claim.
#257Canonical normal form
QuestionIs ∑a ∈ A 1/(2a − 1) irrational for every infinite set A of positive integers?
A set existence question becomes a statement about one canonical greedy orbit, with no freedom to choose a convenient support.
EvidenceLean checked exact equivalence for every nonnegative rational target
Still openProduce cofinal actual skips for 1/2, 1/21 or another unresolved target.
Uses the classical Erdős Borwein irrationality theorem inside a source specific greedy synthesis; no priority claim.
#1041All degree partial theorem
QuestionFor a monic polynomial with every root inside the unit disc, can two roots always be joined by a curve shorter than 2 that stays inside the lemniscate |f| < 1?
The unrestricted geometry has an absolute all degree bound, while the critical level singularity becomes the precise obstruction to the sharp target.
EvidenceAuthored ordinary universal proof with finite regression; no Lean or independent specialist review
Still openReview the component coarea calculation and remove the enlargement from K_mu to K_(2mu).
Classical length area, coarea and lemniscate mechanisms; the exact synthesis was not located in bounded search and no priority is claimed.
The other three programmes
Every claim above links to the thing that carries it: the paper for the written mathematics, the Lean file for the checked statement. The #1041 result is an ordinary written proof, not checked by Lean and not peer reviewed. This is me choosing what to show you first, not peer review, community acceptance, priority or a claim of canonical status.
One machine-checked statement for each problem, and the exact thing that is still unproved: the Eight programme map.
Eight problem papers, for #68, #243, #249, #251, #257, #269, #1041 and #1049, sit inside Plectis’s 13-paper catalogue with the reasoning surfaces and the system papers. They are written for someone reading cold.
Open the papers catalogueRead all eight as pagesOpen the programme map
Lean sourceCheck one theoremRead all eightHow checking worksReproduce the checksCite the corpus
For selected propositions, a second Lean file states the theorem again without its proof. The build checks that the original proof has exactly that type and stays within a fixed axiom budget. This does not review the papers, citations, meaning, novelty or significance.
Trace one classical benchmark after reading the programme and papers. No Lean build is needed. The route returns the statement, exact declaration, Comparator interface, paper and boundary:python3 scripts/verify_claims.py --claim eb_full_support
The whole public record is also published as one packet: a single JSON file you can give to an assistant instead of browsing the pages yourself. It contains every public page and record, each component claim with the limit on that claim, and instructions to cite exact pages.
Download the packet .json save it, then drag the file into ChatGPT, Claude, Gemini or Grok. There is a smaller digest, also JSON, if your assistant refuses a file that size. The reviewer brief is shorter still and carries only the decision layer: what a reader in your position can and cannot conclude from the public record.
The assistant reads and quotes the public files. It cannot run any of the checks. If it tells you it ran one, it is wrong.
I am 22, an economics undergraduate at Bristol. I built this alone over about a year and paid for it myself, and AI was the only tool I used.
The eight problems were picked because they are deep, and I did not expect to solve them. The experiment was to see what happens when you throw as much as you can at problems like these, and to build the infrastructure off the failure modes today's models actually show. I designed the system for coding agents to work in, on the assumption that it gets more useful as the models improve. I have not shown that; it is still an assumption. Most of the mathematics is written in Lean, which checks every step, so you do not have to take my word for those claims. The Erdős problems the work covers are open, and none of it solves one.
It is published so that anyone can continue it. The corpus, the tooling, and the open step each paper names are all public: clone them, run your own models at the problems, or improve the infrastructure itself. A solution found that way is yours, and so is the credit.
Nobody independent has checked the mathematics yet, and nobody outside has seen the whole system. If you can evaluate work like this, the most useful thing is bounded: take one representative public claim, follow it to its source and its evidence, and tell me where the wording goes further than the record does. If you are in a position to look at all of it, I would like to show you. I am also looking for work or funding; a fellowship or something like it would let me do this properly instead of alongside a degree.
