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. All eight remain open, and none of this solves one.
Start here
Five results, stated here. Each gives the question, what was actually proved, what backs it and what is still missing.
#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.
No Lean statement: this one is an ordinary written proof.
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.
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.
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.
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.
