Will CookWill Cook
I’ve been using AI to do maths research and build software. As it produces more complicated work, I also want to make that work easier for other people to understand.
Each project has its own website, and every one is on the map below with its videos and its code. New here? Start with the introduction, which explains how they fit together.
Websites, videos and code
Each line joins a video to the website it explains, and a website to its code on GitHub. Point at anything to see what it connects to.Each website with its videos and its code on GitHub.
Start here
Two introductions to how the projects below fit together.
Videos
Code on GitHub
All public repositories
Plectis Mathematics
Eight Erdős problems I researched with AI, with the papers, computer-checked proofs of partial results and the approaches that failed.
Maths map, on Plectis MathematicsThe papers, on Plectis Mathematics
Videos
Code on GitHub
Research on eight Erdős problems and the system behind it: Lean proofs, papers on research and writing, experiments and open questions.
Lean 4 source for the eight Erdős problem programmes, with selected Comparator and Palomar checks.
Lean Exposition
One result about the Sherrington–Kirkpatrick model of magnets, explained three ways and linked to a map of the argument and its Lean statements.
Argument map, on Lean ExpositionRead the exposition, on Lean ExpositionThe papers as PDFs, on Lean Exposition
Videos
SK reading interface
How different can two nearly best answers be?
Code on GitHub
Pinned Lean evidence and traceable mathematical exposition, with an interactive reading website.
Plectis Atlas
Read OpenAI’s maths papers alongside the reports that outside groups wrote about their claims and proofs.
Lean statements, on Plectis AtlasHow to use the Atlas, on Plectis Atlas
Code on GitHub
An independent reader for OpenAI’s mathematics release: papers, Lean statements and attributed outside readings.
Practical Formal Verification
88 Python components from my research system. For twelve, mathematical proofs show that particular calculations follow precise written requirements.
System map, on Practical Formal VerificationThe 88 components, on Practical Formal VerificationQuickstart, on Practical Formal Verification
Videos
Practical formal verification
Code on GitHub
practical-formal-verification, on GitHub
88 Python components and worked examples for inspecting AI-assisted research.
Zenith
Experiments on whether records of past mistakes help AI models test and repair code.
Videos
Code on GitHub
Experiments on whether an AI tester finds more bugs after seeing its earlier misses, with studies of code repair.
Tools for working with AI agents
These have no website of their own. Their code is on GitHub.
Safety Core, code on GitHub
Keep agent rules in one file and see which are written instructions and which have a program checking commands.
Code on GitHub
An editable rulebook and practical checks for coding agents.
One Checkout, code on GitHub
Commit a selected change while other agents’ unfinished edits stay in the same files.
Code on GitHub
Commit one agent’s fix without including another agent’s unfinished edits.
Code Map
Read saved descriptions of files and follow their recorded code connections in a map.
Videos
Code on GitHub
No public repository. Still in my private system; the film shows it working.
Videos
Nine films are on YouTube and three are in preparation. Each opens on YouTube in a new tab.
Start here
Introduction: using AI for maths research and software, video on YouTube, 5 minutes 44 seconds
In this video I introduce the projects and explain how they fit together, from computer-checked proofs and papers to maps and videos you can follow yourself.
How the projects fit together (first version), video on YouTube, 8 minutes 4 seconds
I go through the maths, the code map, how I make these videos, and the tools I use to manage the agents. Then some research into how the agents could improve their own way of working.
Plectis Mathematics
Open the websiteplectis-erdos on GitHubplectis-erdos-lean on GitHub
Maths Map: how proofs, papers and explanations connect, video on YouTube, 6 minutes 12 seconds
A computer-checked proof can still be difficult for a person to understand. In this video I use the maths map and Erdős problem 257 to explain how I take research done with AI through a long research record, a shorter paper, an explanation paper and finally a video.
Erdős #257: why some infinite sums cannot be fractions, video on YouTube, 30 minutes
Erdős problem 257 asks what happens when you choose infinitely many different entries from 1, 1/3, 1/7, 1/15, and so on, and add them. Must the total be irrational? The full question is still open; in this video I explain a known partial result.
Lean Exposition
SK reading interface
How to read the SK result on its website: the three papers beside a map of the argument, and how to move between their levels of detail.
How different can two nearly best answers be?
The mathematics behind the SK result, starting from four magnets: when two arrangements both have nearly the lowest energy, how differently can they point?
Plectis Atlas
I built Plectis Atlas so you can read OpenAI’s maths papers alongside the reports from groups checking them. In this video I follow one paper about pi and explain why MathVet and Carlos Toledo’s cert-machine give different labels to what was checked.
Practical Formal Verification
Practical formal verification
What the 88 components do and what the proofs behind twelve of them establish, followed through one example: checking how untrusted text moved between an assistant’s steps.
Zenith: can an AI tester learn from the bugs it missed?, video on YouTube, 4 minutes 55 seconds
For this Zenith experiment, I gave an AI model a record of the bugs it had missed and tested whether that helped it catch bugs in new programs.
Tools for working with AI agents
I asked an AI coding agent to fix a typo and commit it in a small test project. When a test failed, the agent supplied a made-up setting so it could commit anyway. I use that experiment to explain Safety Core.
How I commit a finished fix in Git when Claude and Codex have both edited the same file and one agent is still working.
CodeMap: follow a file from its description to its code, video on YouTube, 6 minutes 40 seconds
AI wrote most of the software I use for my research. In this video I go through Code Map, an interface where I can read saved descriptions of the files and follow their connections.
Get in touch
These videos show what I’ve learned to build. I’d love to put those skills to use on other problems. I’m looking for work, an internship, fellowship or funding, and I’m very open to working together. If there’s a problem you think I should try, please let me know.
If something doesn’t make sense, or you spot a mistake, please let me know. If your feedback leads to a change, I’d be happy to credit you, with your permission.