Selected work. Built to be used. Made to be explored.
An independent productMusic, theory & software
♫
Modal Runs
Less thinking about playing. More playing.
A guitar app that hears what you play, shows where you are, and gives you a musical world to explore. I built it from the theory and sound engine through the product around them.
An AI research lab. With a theorem to show for it.
I built a research environment where AI agents explore mathematics and proof kernels check the results. The work includes a formally checked extension of Anthropic's zeta result.
Height shows sampled log magnitude, clipped for display. The orange curve follows the sampled column nearest σ = ½. Explore the function here; the proved result is reported separately.
Four-point certificate proved in Lean
67.28470%
At least this proportion of zeta zeros are simple and on the critical line, as an asymptotic lower bound.Lean × NanoDaIndependently rebuilt
Built on Furman & Alpöge's work at Anthropic: 67.25007% to 67.28470%, an extension of 0.03463 percentage points. The earlier advance from 41.6% to 67.25% is theirs.
What does this mean, in plain English?
Zeta Lab is where I build tools for AI agents to explore mathematics. The agents propose ideas; proof-checking software checks the formal results. The number above is one verified extension of earlier research, with the original work credited alongside it. It does not prove the Riemann Hypothesis.
01 / Explore
Agents work in parallel.
They propose mathematical ideas and test candidates.
02 / Formalize
A claim becomes a proof.
The formal statement and its proof are written in Lean.
03 / Check
The kernels check it.
Lean and NanoDa independently rebuild the registered result.
Explore the critical lineAn interactive numerical study +
ζ(½ + it) / Hardy's ZComputed here
tzeros in viewfound
Each dot is a sign change of Hardy's Z, computed in your browser. This numerical study is separate from the formal proof. The registered result is a verified asymptotic bound, not a proof of the Riemann Hypothesis; kernel checking is separate from peer review.
AI research tools. Agents exploring ideas. Results you can check.
AI agents trained a small transformer and proved in Lean that it adds correctly on every input pair. They then built a Lean check of a safety certificate for an ACAS Xu network. The transformer result covers all input pairs; the ACAS result covers the specified property-1 input box. A separately implemented proof checker rechecked each theorem's exported dependency closure.
Every cell and every leaf is a checked case. Point at one.
The square of pairs: each cell (a, b) is shaded by the answer the theorem proves the model returns, (a + b) mod 113. The leaf plane: a projection of the 34 five-dimensional leaf boxes onto X₁ and X₂, with 32 distinct rectangles and two symbolic dividers for X₀ splits; the teal box is leaf 38, the smallest checked margin. Both drawings visualize the checked results; the kernel checked arithmetic certificates and coverage, not these images. The results are reported beside them.
Trained transformer proved in Lean
12,769
A trained one-layer, four-head transformer with integer weights and exact real softmax adds modulo 113 correctly on every input pair.Lean × NanoDaRead the proof story
Tiny model, toy task, brute force over all inputs: this proves the integer-rounded model, not the float checkpoint. Released proof objects and checks.
Prior work: Brian Naughton's certified-grokking certifies the same architecture with a trusted Python interval core; Jason Gross's Coq work proves accuracy for trained max-of-two transformers. The model and trust boundaries differ.
ACAS Xu certificate checked in Lean
34/34
All 34 leaves checked and the input box covered. AI agents built a Lean check of an alpha-beta-CROWN certificate for ACAS Xu network 1_1, property 1, using TorchLean and the VNN-COMP benchmark.Lean × NanoDaRead the ACAS evidence
Exact real semantics, standard axioms only. The ONNX importer is audited, not proved. No IEEE execution or aircraft claims.
What does this mean, in plain English?
Two small neural networks, and for each a theorem that Lean's proof kernel accepted: the transformer gives the right answer for every one of its 12,769 possible inputs, and the ACAS Xu network stays below the stated threshold everywhere in the stated input box. AI agents wrote the proofs; two independent proof checkers accepted them. It says nothing about large models, floating-point hardware or aircraft.
Small networks. Whole input ranges. Proofs a kernel accepted.
Since 2025, voice agents I built have answered the phone for a limo brokerage in two US markets. The agent quotes from live rate logic, places the card hold, and hands the booking to a person for review. Real customers, real money, three in the morning included.
In production, not a demo. I ran that operation from 2019 before I wrote the software that runs it.
At some point I sorted 168 GarageBand and Logic projects into four folders: Good, Bad, Meh, and Magic. It turns out 65% of the files with a key attached are in A minor or C major. Yep. I feel seen.
I've played guitar for more than 25 years. I improvise blues and space rock, mess with electronic music, study because I enjoy it, and generally follow whatever gives me dopamine at the moment.
Bruno is my one-year-old tricolor Sheltie. His full imperial name is Brutus Maximus Aurelius. He is used to long walks. I love him.
