Math + CS at KREA University, formerly Chennai Mathematical Institute. I build computational tools for combinatorics, formal verification, and education.
BSc (Hons.) Mathematics and Computer Science at KREA University, previously at Chennai Mathematical Institute. I work at the intersection of computation and pure math, with a preference for problems where you can verify conjectures by brute-forcing them on a cluster.
Currently doing formal verification consulting, teaching math to 100+ middle schoolers, and tutoring olympiad students (IMO/INMO qualifiers). Research spans SAT-based Ramsey theory, topological anti-cheat methods, and ML for open conjectures. I write about all of it on Substack.
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. Worked on formalizing the Erdos-Szekeres conjecture under a professor.
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.