Will Cook

I do mathematics research and build software with AI agents. I also build ways to inspect what the agents produce.

That means Lean proofs of AI-written mathematics, websites that display a paper beside its Lean code, and tools for running several coding agents in one repository. The introduction video explains how the projects fit together.

Mathematics and LeanFive projects
Tools for AI coding agentsFive projects
Verification and evaluationTwo projects

I’m looking for a job, internship, fellowship or research collaboration. How to reach me

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

Projects

Several projects use Lean, a proof assistant: software that accepts a proof only after verifying every step.

Mathematics and Lean

Plectis Mathematics
AI-assisted research on eight Erdős problems, with papers, records of failed approaches and Lean 4 proofs of partial results.
Seven original questions remain open. The #1041 formal-statement counterexample is due to ani. The papers are not peer reviewed.
Open the website: Plectis Mathematics
On the website
Maths map, on Plectis Mathematics
The eight problems, on Plectis Mathematics
The papers, on Plectis Mathematics
Each problem page states whether the original question is still open and which statements the Lean proofs cover.
Videos
- Maths Map: eight Erdős problems on one map, video on YouTube, 6 minutes 20 seconds
  I use one problem, Erdős #257, to show where its proof, papers and explanation video are on 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
  Papers, Lean proofs, experiments and open questions from the research on eight Erdős problems, and papers on how the research was done.
- plectis-erdos-lean, on GitHub
  Lean 4 source for the eight problems. Comparator accepted selected proofs against separately written statements, and Palomar, an online proof registry, reran some of them.
Quartic Reader
Lean 4 formalisation of OpenAI’s nearly quartic randomized–quantum query-complexity separation, with mathematical expositions and a paragraph-linked proof reader.
Original theorem by OpenAI; formalisation and explanations made with AI. No human has reviewed whether the Lean statements match the paper.
Open the website: Quartic Reader
On the website
Read OpenAI’s paper, on Quartic Reader
General reader, on Quartic Reader
Comparator accepted each proof bundle in local runs on my computer and rejected five deliberately wrong solutions. The Forrelation lower bound, which the preprint imports, is proved here by a shorter route in a weaker form.
Code on GitHub
- quartic-query-lean, on GitHub
  The Lean proof of OpenAI’s nearly quartic separation, three written explanations of the argument, and the reader website’s source.
Lean Exposition
Three explanations of OpenAI’s full-support theorem for the Sherrington–Kirkpatrick spin glass, linked to Lean declarations and an argument map.
The theorem and Lean proof are OpenAI’s. I made the explanations and links with AI; no mathematician has reviewed them.
Open the website: Lean Exposition
On the website
Argument map, on Lean Exposition
Read the exposition, on Lean Exposition
The papers as PDFs, on Lean Exposition
The site lists each Lean build and the statements it covers. Comparator gave no verdict on either theorem.
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
  The three papers, the Lean they link to at a fixed version, and the source of the reading website.
Proof Reader
Read Contextual Embeddings (PLDI 2026) beside its authors’ Lean proof, with statement-to-code links and a graph of proof dependencies.
Paper and proof by Frohlich, Foster, Kavvos and Wang. I made the reader and links with AI; the authors have not reviewed the links.
Open the website: Proof Reader
On the website
Read Contextual Embeddings, on Proof Reader
Code on GitHub
- proof-reader, on GitHub
  Each paper is one folder, and any paper with public Lean can be added. A program compares the site’s text with the PDF word for word.
Plectis Atlas
An index of OpenAI’s mathematics manuscripts, Lean statement files and published assessments, grouped into 372 paper families.
Reports credited to MathVet, Carlos Toledo’s cert-machine and Neal McBurnett. I assembled the index and statement links with AI.
Open the website: Plectis Atlas
On the website
Example: two reports on a paper about π, on Plectis Atlas
Lean statements, on Plectis Atlas
How to use the Atlas, on Plectis Atlas
I drafted the matches between each Lean statement and its paper with AI; no person has reviewed them.
Videos
- Atlas: why two people gave one OpenAI maths paper different verdicts on its completeness, video on YouTube, 5 minutes 35 seconds
  In two reports on an OpenAI paper about π, both groups say Comparator accepted the Lean proof, but they label the Lean statement’s coverage differently. I go through what each label means.
Code on GitHub
- plectis-atlas, on GitHub
  The Atlas website’s source: OpenAI’s maths papers, their Lean statements, and outside groups’ reports credited to their authors.

Tools for AI coding agents

Agent Trace
Local Codex and Claude Code session viewer with tool traces, selective context export and optional MCP access.
Technical preview; browser app or native Mac window.
Code on GitHub: Agent Trace
Code on GitHub
- agent-trace-mechanism, on GitHub
  The session viewer and the optional MCP server for Codex and Claude Code logs. Install it with pip and run agent-trace-app.
One Checkout
Commits a reviewed Git patch while preserving another agent’s unfinished staged and working-tree edits, including changes 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.
Safety Core
Generates AGENTS.md, CLAUDE.md and command-enforcement hooks from one rulebook, distinguishing written instructions from rules enforced by hooks.
Tested in one small Claude Haiku study; the enforcement rule was written after observing the failure.
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 give a coding agent written rules and command-blocking hooks, then record what it does to get past a failing test.
Code on GitHub
- safety-core, on GitHub
  A rule file for coding agents and the hooks that block commands a rule forbids.
Code Ontology Bridge
Exports Python code structure to DuckDB, with semantic descriptions and recursive SQL views for NVIDIA Auto Ontology’s text-to-SQL agent.
Independent of NVIDIA. Descriptions helped DeepSeek in a 48-question direct-prompt study; no clear improvement in the 12-question Auto Ontology study.
Open the website: Code Ontology Bridge
On the website
The study, on Code Ontology Bridge
Caller example, on Code Ontology Bridge
AI models wrote the questions and answer keys; 21 answer keys were corrected after the runs. Every question, answer and failed run is published.
Code on GitHub
- code-ontology-bridge, on GitHub
  The exporter, the DuckDB schema, the Auto Ontology table descriptions and the 48-question study with every answer.
Code Map
A code browser with docstring descriptions and function-call links, available to both the human reader and coding agents.
Private software; the video shows it in use.
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. Not released; the video shows it in use.

Verification and evaluation

Practical Formal Verification
Dafny proofs for 16 selected computations in an 88-component research-workflow prototype, with generated Python and proof-coverage maps.
The proofs cover those computations, not the complete system.
Open the website: Practical Formal Verification
On the website
The component map, on Practical Formal Verification
All 88 components, on Practical Formal Verification
Which proofs and tests cover each one, 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
  On a map of the 88 Python components, I show what each Dafny proof and saved result covers.
Code on GitHub
- practical-formal-verification, on GitHub
  The components, their Dafny proofs, the Python compiled from them and worked examples.
Zenith
Experiments on whether records of earlier mistakes help language models test and repair code. A held-out study found 77.0% versus 69.2% fault-class detection.
One model on 58 HumanEval problems; about half the gain came from timeouts. Study available in an unmerged branch.
Code on GitHub: Zenith
On the website
Website for the earlier studies, on Zenith
Held-out study (unmerged revision), on Zenith
Study pull request #13, on Zenith
Earlier paper on program repair (PDF), on Zenith
The held-out study used DeepSeek V4.1 Flash. The earlier website and PDF describe separate studies, including program repairs rising from 259 to 365 of 576 tasks.
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
  Code, data and paper for the experiments on showing an AI tester the bugs it missed, and the code-repair studies.

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

I’m looking for a job, internship, fellowship or funding, and I’m open to working with other people on their problems. If there’s a problem you think I should work on, please email me.

If something on these pages is unclear or wrong, please tell me. If your feedback leads to a change, I’d be happy to credit you, with your permission.