Will Cook
Plectis · research with AI, mathematics and software
I built Plectis to pursue research I found interesting with AI. I choose a direction, prepare the work for people who can interpret it, and use their corrections to decide what to do next. The system keeps that work together across conversations, including the papers, proofs and failed attempts.
Public work
Work through one example with optional hints and its sources. No installation needed.
Watch the walkthrough, 4:57 to see the research software, or read how the system works.
Explore Plectis for the maps, papers and other demonstrations.
Mathematics · eight programmes; ani's #1041 example refutes an exact Formal Conjectures length statement
Hover or focus a problem to preview it; activate the link to open its page.Open a problem page:
Erdős #68 The factorial-denominator series · original problem remains open
Erdős #243 Reciprocal-tail rigidity near the Sylvester recurrence · original problem remains open
Erdős #249 The binary totient series · original problem remains open
Erdős #251 The prime-gap dyadic series · original problem remains open
Erdős #257 Reciprocal sums over infinite exponent supports · original problem remains open
Erdős #269 Three-prime running least common multiples · original problem remains open
Erdős #1041 Short connections inside polynomial lemniscates · exact Formal Conjectures path-image bound refuted; historical curve-length correspondence unreviewed
Erdős #1049 Lambert-type series at rational bases · original problem remains open
Mathematics repository · formal source and ways to continue the work
Take part
Try an experiment on the public Lean corpus, work on an open problem or suggest a better way to run and check the work. The contribution guide shows how to send an idea, correction, proof or infrastructure proposal and how each is credited.
For a small example, try multiplying approximations. The question is whether their error bounds guarantee the product’s accuracy. The note credits the original theorem and includes an exact arithmetic checker.
Read with an AI
Full AI packet and guided tours · Short reviewer brief · Full paper text and reading routes
Reading these files does not run the checks.
About me
My background is economics, and my mathematical knowledge is limited. I built the research system with AI coding agents, set the objectives and review criteria, direct the work and decide what to release. Agents wrote the code and drafted and revised the papers. Each paper records the earlier mathematics and other people's contributions it draws on.
Code Map and Agent Trace, shown in the films, are part of my private research software. The public Lean repository lets you inspect and continue the mathematical work.
If you try the research task, tell me what you tried and where you got stuck. I am also looking for people who want to use or develop the research system with me, through collaboration or support.
After a model produces a proof
The AI-and-mathematics essays ask who does the work that makes a result useful. Henry Cohn places responsibility on the producer. Grant Sanderson asks for explanations that show why a construction is worth trying. These are useful standards for this project: retain failed approaches, explain the difficult step and let a reader test a changed assumption.
Timothy Gowers raises a fair alternative: perhaps a reader can simply ask an LLM. The maintained record has to earn its place by helping someone check or continue a particular investigation. The task gives you one way to try that. A checked proof and a readable explanation do not, by themselves, show that somebody understands the mathematics.