Will 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 or code, and its videos. New here? Start with the introduction, which explains how they fit together.

See the eight projects

Introduction (V3): I still want to understand what AI builds, video on YouTube, 5 minutes 37 seconds

Projects

Visit a project directly, or choose Show details to see its videos and code here.Each project with its videos and its code on GitHub.

Mathematics

Plectis Mathematics
Eight Erdős problems I researched with AI, with the papers, computer-checked proofs of partial results and the approaches that failed.
Open the website: Plectis Mathematics
On the website
Front page, on Plectis Mathematics
Maths map, on Plectis Mathematics
The eight problems, on Plectis Mathematics
The papers, on Plectis Mathematics
The original questions remain open where the problem pages say so.
Videos
- Maths Map: eight Erdős problems on one map, video on YouTube, 6 minutes 20 seconds
  I use Erdős #257 to show how to find a proof, its papers and an explanation video through the Maths Map.
- Erdős #257: why some infinite sums cannot be fractions, video on YouTube, 30 minutes 8 seconds
  I explain a known irrationality result for Erdős #257, starting with 1, 1/3, 1/7, 1/15, and so on.
Code on GitHub
- plectis-erdos, on GitHub
  Research on eight Erdős problems and the system behind it: Lean proofs, papers on research and writing, experiments and open questions.
- plectis-erdos-lean, on GitHub
  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.
Open the website: Lean Exposition
On the website
Front page, on Lean Exposition
Argument map, on Lean Exposition
Read the exposition, on Lean Exposition
The papers as PDFs, on Lean Exposition
The three accounts are drafts. The site shows their reviews and what each check covers.
Videos
- Lean Exposition: read a maths paper beside its argument map, video on YouTube, 3 minutes 59 seconds
  I show how to read a maths explanation beside a map of its assumptions, results and sources.
- Spin glasses: how different can two nearly best answers be?, video on YouTube, 12 minutes 28 seconds
  I explain how two nearly best arrangements of magnets can differ, starting with four arrows.
Code on GitHub
- lean-exposition, 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.
Open the website: Plectis Atlas
On the website
Front page, on Plectis Atlas
Lean statements, on Plectis Atlas
How to use the Atlas, on Plectis Atlas
Videos
- Atlas: why two people gave one OpenAI maths paper different verdicts on its completeness, video on YouTube, 5 minutes 35 seconds
  I compare two checking reports for an OpenAI maths paper about pi, using Plectis Atlas.
Code on GitHub
- plectis-atlas, on GitHub
  An independent reader for OpenAI’s mathematics release: papers, Lean statements and attributed outside readings.

Software and experiments with AI agents

Practical Formal Verification
88 Python components from my research system. For twelve, mathematical proofs show that particular calculations follow precise written requirements.
Open the website: Practical Formal Verification
On the website
The component map, on Practical Formal Verification
All 88 components, on Practical Formal Verification
What each one is checked by, on Practical Formal Verification
Documentation, on Practical Formal Verification
Videos
- Formal verification: what does this check actually prove?, video on YouTube, 5 minutes 12 seconds
  I show what the proofs and saved checks cover in a map of 88 Python components.
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.
Code on GitHub: Zenith
On the website
Front page, on Zenith
The paper (PDF), on Zenith
Small research studies, with their limits described in the repository.
Videos
- Zenith: I showed an AI tester the bugs it missed, video on YouTube, 5 minutes 3 seconds
  I test whether an AI code tester catches more bugs after seeing a record of its earlier misses.
Code on GitHub
- plectis-zenith, on GitHub
  Experiments on whether an AI tester finds more bugs after seeing its earlier misses, with studies of code repair.
Safety Core
Keep agent rules in one file and see which are written instructions and which have a program checking commands.
Code on GitHub: Safety Core
Videos
- Safety Core: my AI agent made up a setting to pass a test, video on YouTube, 8 minutes 56 seconds
  Video, 8:56
  I test written rules and command checks on a coding agent that tries to get past a failing test.
Code on GitHub
- safety-core, on GitHub
  An editable rulebook and practical checks for coding agents.
One Checkout
Commit a selected change while other agents’ unfinished edits stay in the same files.
Code on GitHub: One Checkout
Videos
- One Checkout: when Claude is done and Codex is still editing, video on YouTube, 5 minutes 35 seconds
  Video, 5:35
  I show how to commit one fix while another agent's unfinished edits stay in the same file.
Code on GitHub
- one-checkout, 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.
Watch the video: Code Map
Videos
- CodeMap: finding my way through code written with AI, video on YouTube, 6 minutes 49 seconds
  Video, 6:49
  I follow a code search from a file's saved description to the function and the code that calls it.
Code
No public repository. Still in my private system; the film shows it working.

Videos

13 videos are on YouTube. Each opens on YouTube in a new tab.

Earlier introductions

Older versions, kept for reference. Start with Introduction (V3) above.

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.