Electrical engineer · Atlanta, GA
I design and build test equipment for aircraft avionics at Delta TechOps. Outside of work, I’m usually in the middle of a side project or two.
I’m an electrical engineer at Delta TechOps in Atlanta, where I build automated test equipment for avionics components. I work on every part of it, from the schematics and board layout to the test software, assembly and validation. I have a B.S. in electrical engineering from Georgia Tech.
Lately, most of my side projects have been math, mainly fast transforms and number theory. Several come with machine-checked proofs in Lean 4.
A 260,032-parameter language model packed into one 595 KB PostScript file. Send it to a laser printer, and the printer’s own processor writes and typesets a children’s story about printers. The computer that sent it does none of the math.
Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore.
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.
View on GitHub: wht-fewer-operationsIn 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.
View on GitHub: sieve-ceilingsOn 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).
View on GitHub: qrh-zero-free-bounds