I use AI to make AI-written maths and code easier to understand.
I do maths research and build software with AI. Most projects here can be followed at several levels of detail, from a short video down to the proof or the code.
I build the tools so they get better as AI models get better.
The projects
Fifteen projects in five groups. Each has its own page, from a short video down to the proof or the code.
Three places to start
These three are my examples in the introduction, one each from maths, code and working with AI coding assistants.
All fifteen, by group
1 Maths
Research on Erdős problems and on two of OpenAI’s results, as papers, websites and proofs in Lean.
Lean is a program that checks mathematical proofs.
The funnel: How a Lean proof becomes papers and a video
Maths Map: Eight Erdős problems on one map
Erdős #257: A case from 1968, proved and checked in Lean
Quantum computers: OpenAI’s fourth-power result, proved again in Lean
Spin glass: Two nearly best answers, half the arrows differ
Reader websites: Click a linked sentence, open the Lean beside itLean Exposition, Quartic Reader, Proof Reader
2 What a check covers
Which statement a proof or a report covers, and what it leaves out.
3 Code
Code turned into a map, and into a database that an AI model can search.
4 AI coding assistants at work
Tools for working with AI coding assistants, and experiments on what they do.
5 How I make these videos
The plan I write before AI draws any animation.
About
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.