Skip to research and reading routes

Will Cook

Plectis · open-source mathematics

I’m building Plectis, an open-source mathematics project. We use AI and Lean to work on eight open problems, and publish the results, proofs and unfinished work so others can continue it. I direct the work and am responsible for the released claims.

The research and how to join

Start with the research.

Choose a problem to see its question, results and remaining work. You can read everything in your browser.

Explore the eight problems

Contributors receive credit for their work. If you solve a problem, the result and credit are yours and your collaborators’. How credit works

How this project works — Problem-Sized Lean Worlds

How to contribute — From Spare Compute to Cumulative Mathematics

Source code and contribution instructions

Lean repository and README · Contribution instructions

Browse the problem notes here

In numerical order. Each short note describes one problem; the longer records retain additional working context.

Lean checks formal statements. It does not establish novelty, significance or peer review.

All papers and PDFs · Glossary

Read it with an AI

Give the full papers and a reading map to an AI assistant in one JSON file.

Download the full text and routes .json

How to use the file · smaller versionssave 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 file supplies the public files; reading it does not run the checks. A claim that a check passed needs evidence from actually running it.

About me and why I built this

Why it is here

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.