Skip to the questions
Will Cook(my name)

Use AI to make what AI produces easier to understand, at every level of detail.Build things that get better as AI models get better.

1:37

Short introduction · 1:37Introduction: Using AI to explain maths and codeMeet the maths funnel, Code Ontology Bridge for NVIDIA Auto Ontology, and Agent Trace: three ways to make AI output easier to follow.

Mathematics

Erdős problems: AI-assisted proofs in Lean 4 Maths Map Show the projectHide
1:49

Short video · 1:49Maths Map: eight Erdős problems and their papersFind a theorem on Maths Map, open its paper, and see the available Lean and Comparator checks.

Maths Map

Erdős problems · Lean 4 · Comparator

AI-assisted research on eight Erdős problems: a research record and paper for each, Lean 4 proofs of partial results, and Comparator results where they exist.

Open the website

More videos

Code

  • plectis-erdos 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 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.
Maths papers linked to their Lean 4 formalisations Quartic Reader · SK Reader · General Reader · Plectis Atlas Show 4 projectsHide

One video covers Quartic Reader, SK Reader and General Reader

1:27

Short video · 1:27Quantum Reader: Open the Lean proof of OpenAI's fourth-power query boundFollow a passage in Quartic Reader to its linked Lean statements and the labels describing how they match.

Quartic Reader

Quantum query complexity · Lean 4

OpenAI's nearly quartic separation between randomized and quantum query complexity, formalised in Lean 4. Each paragraph of the paper links to the Lean declarations it states.

Open the website

More videos

Code

  • quartic-query-lean The Lean proof of OpenAI’s nearly quartic separation, three written explanations of the argument, and the reader website’s source.
1:32

Short video · 1:32Lean Exposition: Open the Lean proof of OpenAI's spin-glass theoremClick a statement in SK Reader’s papers to open the linked part of OpenAI’s Sherrington–Kirkpatrick Lean proof.

SK Reader

Sherrington–Kirkpatrick spin glass · Lean 4

Three expositions of OpenAI's full-support theorem for Sherrington–Kirkpatrick spin-glass minimisers. Each passage links to the Lean 4 declarations of OpenAI's proof.

Open the website

More videos

Code

1:30

Short video · 1:30Proof Reader: Open Lean code linked to a paper's sentenceTry General Reader on Contextual Embeddings: click a sentence to open the corresponding lines of the authors’ Lean proof.

General Reader

PLDI 2026 paper · Lean 4

Contextual Embeddings (PLDI 2026), each sentence linked to the authors' Lean proof, with a declaration dependency graph and the axioms used. Any paper with public Lean code can be added.

Open the website

Code

  • proof-reader 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.
1:42

Short video · 1:42Atlas: Two coverage labels for OpenAI's paper about πFind OpenAI’s maths papers in Plectis Atlas, then compare MathVet and cert-machine’s different coverage labels for one paper about π.

Plectis Atlas

OpenAI's 719 maths papers · Lean statements

An index of OpenAI's 719 maths papers in 372 families, with their Lean statement files and the coverage labels outside reviewers such as MathVet and cert-machine assigned.

Open the website

More videos

Code

  • plectis-atlas The Atlas website’s source: OpenAI’s maths papers, their Lean statements, and outside groups’ reports credited to their authors.
From one Lean proof to papers and a narrated video The funnel · Narration IR Show 2 projectsHide
2:12

Short video · 2:12How I use AI to turn a Lean proof into three papers and a videoFollow a Lean proof of a case of Erdős #257 into a research record, specialist paper, exposition and video.

The funnel

Lean 4 → papers → video

A worked example of turning one Lean proof, a 1968 case of Erdős #257, into a research record, a specialist paper, an exposition and a video.

Open the code on GitHub

More videos

Code

  • lean-exposition The three papers, the Lean they link to at a fixed version, and the source of the reading website.
2:20

Short video · 2:20Narration IR: Time an arrow's movement to spoken wordsPlan what one spin-glass sentence means, attach an arrow’s turn to spoken words, and locate its source quotations.

Narration IR

Narration → animation plan

An intermediate representation between a narration script and its animation: what each sentence must explain, its source quotations, and picture changes timed to spoken words.

Open the code on GitHub

More videos

Code

  • narration-ir The portable skill, references, worked example and optional Python tools for validation and scene briefs.

Software

Claude Code and Codex: session logs, Git commits and hooks Agent Trace · One Checkout · Safety Core Show 3 projectsHide
2:25

Short video · 2:25Agent Trace: Read Claude Code and Codex commands and resultsInspect saved Claude Code and Codex sessions, see commands beside their output, and copy selected context into another chat.

Agent Trace

Claude Code · Codex · MCP

A local viewer for Claude Code and Codex session logs: every tool call with its output, export of a chosen level of detail to another chat, and an optional MCP server.

Open the code on GitHub

More videos

Code

  • agent-trace-mechanism The session viewer and the optional MCP server for Codex and Claude Code logs. Install it with pip and run agent-trace-app.
1:28

Short video · 1:28One Checkout: Commit one fix while another AI edits the same fileCommit one agent’s Git patch while another agent’s unfinished edits stay in the same file.

One Checkout

Git · parallel coding agents

Commits one agent's reviewed Git patch on top of HEAD while other agents' staged and unstaged edits stay in the working tree, including edits to the same files.

Open the code on GitHub

More videos

Code

  • one-checkout Commit one agent’s fix without including another agent’s unfinished edits.
1:25

Short video · 1:25Safety Core: 6 of 10 AI runs committed with rules, 0 with a command checkIn one retry test, a made-up setting reached a commit in 10 of 10 runs, six under written rules, none under hooks.

Safety Core

AGENTS.md · CLAUDE.md · Claude Code hooks

Generates AGENTS.md, CLAUDE.md and Claude Code hooks from one rulebook, so selected rules are enforced before a command runs rather than only written as instructions.

Open the code on GitHub

More videos

Code

  • safety-core A rule file for coding agents and the hooks that block commands a rule forbids.
Codebase maps and the NVIDIA Auto Ontology bridge CodeMap · Code Ontology Bridge Show 2 projectsHide
2:10

Short video · 2:10CodeMap: A map of my code from AI-written file descriptionsExplore CodeMap’s file boxes and the descriptions coding agents saved in the code; fetch those same descriptions as text.

CodeMap

Docstrings · call graphs

A code browser built from docstrings that agents write in a fixed format: a description of every file and links along function calls, readable by people and by coding agents. Not released.

Not released; the videos show it in use.

More videos

Code

Not public.

1:35

Short video · 1:35NVIDIA's Auto Ontology: 10.3 of 12 questions about its own code correctWith a DuckDB code database, NVIDIA Auto Ontology using DeepSeek averaged 10.3 correct answers out of 12; DeepSeek alone averaged 3.2.

Code Ontology Bridge

NVIDIA Auto Ontology · DuckDB · SQL

Static analysis exports Python functions and call relations to DuckDB with recursive SQL views, so NVIDIA Auto Ontology's text-to-SQL agent can answer questions about a codebase.

Open the website

More videos

Code

  • code-ontology-bridge The exporter, the DuckDB schema, the Auto Ontology table descriptions and the 48-question study with every answer.
Experiments: LLM-written tests and Dafny-verified code Zenith · Practical Formal Verification Show 2 projectsHide
1:54

Short video · 1:54Zenith: AI found 69% vs 77% of bug types per program, without and with past missesOn 58 held-out problems, showing DeepSeek V4.1 Flash its missed bugs raised its average score from 69% to 77%.

Zenith

LLM test generation · DeepSeek · HumanEval

Experiments on whether a record of missed bugs improves LLM-written unit tests: DeepSeek V4.1 Flash's mean fault-detection score rose from 69.2% to 77.0% on 58 held-out HumanEval problems; about half the gain came from timeouts.

Open the website

More videos

Code

  • plectis-zenith Code, data and paper for the experiments on showing an AI tester the bugs it missed, and the code-repair studies.
1:57

Short video · 1:57Formal verification: What a proof covers in my 88-component toolkitExplore an 88-component software map and see exactly which calculations have Dafny proofs.

Practical Formal Verification

Dafny · Python

Dafny proofs for 16 computations in an 88-component Python research toolkit, compiled to Python, with maps of which components each proof covers.

Open the website

More videos

Code

Every video, including earlier editions Search all the work Glossary of terms