ProjectsPublic projects
Here are my math side projects so far. Each one has its own public repo on GitHub.
Lean
A Lean 4 proof that one fixed program computes the discrete Fourier transform of every length with an operation count that grows slightly more slowly than n log n. The proof uses OpenAI’s own problem statement and cost model and builds on a circuit by Marius-Paul Dumitrean from a community repository. I set the goals and directed a team of AI agents (Claude Opus 5.5), which wrote the Lean proofs and ran the searches.
Repo descriptionLean 4 proof: discrete Fourier transform of every length in O(n (log n)^z), z = 1 - 1.7887045e-3, in the RAM model of OpenAI's family 130; and the search for larger savings
View on GitHub: wht-power-saving-lean→Python
Circuits for the Walsh–Hadamard transform that use fewer operations than the textbook method, with Lean 4 proofs of the operation counts. On an FPGA they need fewer logic cells, but on a processor they save only a few percent of run time at best. I directed the work, and AI agents (Claude Opus 5.5) wrote the code and proofs and ran the searches.
Repo descriptionCircuits for the exact Walsh-Hadamard transform with fewer operations: (5/6) N log2 N + N gates on 8^j points, and (3/4) N log2 N + N/4 multiply-adds on 2^k points, both proved in Lean 4. A better constant, not a better exponent.
View on GitHub: wht-fewer-operations→TeX
In 2021, Jori Merikoski proved that infinitely many primes have the form x² + (y² + 1)². His proof finds at least 60% of the expected number, counted with his weights. This paper shows that the same estimates give at least 96.36%, and that 96.36% is the most they can give in Ford and Maynard’s model. I did the work with AI agents (Claude Opus 5.5), and a separate agent checked each step by trying to break it.
Repo descriptionMerikoski's estimates for primes x² + (y² + 1)² give at least 96.36% of the expected count, the most such estimates can give in Ford and Maynard's model: paper, Python checks, history
View on GitHub: sieve-ceilings→Lean
On the Quasi-Riemann Tracker, people are working to lower θ, the boundary past which no Dirichlet L-function can have a zero. My Lean-checked bound, θ = 0.8739558, was merged and stayed the tracker’s best for most of a day, though others have since gone well below it. The repository also maps 66 dead ends for anyone going after a bigger improvement. I did the work with the help of AI agents (Claude Opus 5.5).
Repo descriptionMy work on the Quasi-Riemann Tracker: a map of 66 dead ends below the record with its scripts, Lean proofs of θ = 0.8739558 (merged), 0.8739167 and 0.873903, a conditional θ = 0.8735111, the history, and replay tools
View on GitHub: qrh-zero-free-bounds→Python
A way to size up a proof method before spending weeks on it. You list the clues the method can use and find the best “impostor” that matches every clue but isn’t the real thing. Then you work out how far a new clue would move the method’s limit. It includes four worked examples from analytic number theory and fast algorithms. I did the work with the help of AI agents (Claude Opus 5.5).
Repo descriptionBarrier sheets: what a proof method can reach, the impostor that stops it, and what a new clue is worth; four worked examples
View on GitHub: periodic-table-of-obstructions→
More on GitHub.