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.

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

10:31Full video · 10:31Tour the maths, software and explanation projects, see how they connect, and choose a first video.

Mathematics

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

1:49

Short video · 1:49Find 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

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

4:58Full video · 4:58Compare SK Reader, Quartic Reader and General Reader: paper links, argument maps, formal dependency graphs and the Lean behind them.

1:27

Short video · 1:27Follow 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

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:32Click 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

Code

lean-exposition The three papers, the Lean they link to at a fixed version, and the source of the reading website.
lean-exposition-site The published SK Reader website, built from lean-exposition.

1:30

Short video · 1:30Try 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:42Find 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

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:12Follow 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

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:20Plan 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

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:25Inspect 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

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:28Commit 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

Code

one-checkout Commit one agent’s fix without including another agent’s unfinished edits.

1:25

Short video · 1:25In 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

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:10Explore 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.

Code

Not public.

1:35

Short video · 1:35With 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

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:54On 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.