Computational math, formal verification, and making olympiad students dangerous. I write about it on Substack.
I work at the intersection of computation and pure math. SAT solvers for Ramsey theory, proof assistants for formalizing conjectures, neural nets for number theory. I also teach - olympiad prep (students have qualified to IMO, INMO, EGMO) and introductory math for 100+ kids.
Using cube-and-conquer SAT solving (Kissat + march_cu) to compute 2-color Rado numbers for linear equations. Verified the Ahmed-Zaman-Bright conjecture 2.1 and discovered a new pattern: R2(ax + by = az) = a2, verified for a > 30. Applying PySR symbolic regression to search for closed-form expressions across equation families.
Developed a topological method to identify likely cheaters in online FPS games by modeling player crosshair position on 2-spheres, fitting von Mises-Fisher distributions, and clustering anomalies with HDBSCAN.
Training a neural network to predict Collatz stopping times from binary representations. Exploring whether learned structure in stopping times can tighten known bounds on the conjecture.
Self-taught dependent type theory by automating proofs of olympiad-style number theory problems. Working on formalizing the Erdos-Szekeres conjecture.
Computer vision pipeline for VCT NA Challengers. Detects players, reads scoreboards and maps from broadcast footage using YOLO + custom CNNs. Tracks player performance across matches.
End-to-end pipeline for computing Rado numbers. Generates SAT encodings, runs cube-and-conquer with Kissat/march_cu, then feeds results to PySR for symbolic regression. Discovered the R2(ax+by=az) = a2 pattern.
Self-hosted task management and project notes system. Single-file HTML dashboard with Python API backend. Focus view, weekly review, and project scratchpads. Built to run on a home server.
Recent posts from jeffdoesmath on Substack.
Get new posts delivered to your inbox.
Best way to reach me is email. Also around on GitHub and Substack.