about.
I'm a fourth year undergraduate at Carnegie Mellon University, double majoring in Mathematics and Computer Science with a concurrent master's degree in Mathematics.
My primary line of research is on machine learning for mathematics, and more generally, AI for science. I also study higher category theory, homotopical algebra, and type theory. I'm jointly advised by Prof. Jeremy Avigad, Prof. Sean Welleck, and Prof. Prasad Tetali, and am a researcher in the Hoskinson Center for Formal Mathematics, the Language Technologies Institute, the L3 Lab, and the Institute for Computer-Aided Reasoning in Mathematics. I am the cofounder of Stagira Labs, a research lab focused on using game theory and multi-agent RL to scale AI for scientific discovery. I am also part of the Homotopy Type Theory (HoTT) group and the Higher Category Theory reading group at CMU. Previously, I also worked with Prof. Po-Shen Loh on scaling AI-assisted theorem proving on math competition problems at Expii, and ran The Purple Hand, an anti human trafficking nonprofit.
Recently, I also won the Richard A. Moore Award and was named an ACS Scholar.
My Erdos number is 2.
cLean milestone report released
Named as an ACS Scholar
Public release of Agora v0.1
Won the Richard A. Moore Award in Mathematical Sciences
Presented ImProver at ICLR 2025 in Singapore
Attended the Simons Institute and SLMath joint workshop on AI for Mathematics
research.
My research focuses on automated theorem proving and machine learning for formal mathematics. I'm particularly interested in developing AI systems that can assist mathematicians in discovering and verifying theorems in interactive proof assistants like Lean 4.
My work spans reinforcement learning for proof search, proof optimization techniques, and building tools that make formal verification more accessible to researchers and practitioners. I believe that AI-assisted theorem proving can accelerate mathematical discovery and improve software verification.
ImProver²: Iteratively Self-Improving SLM's for Neurosymbolic Proof Optimization
Riyaz Ahuja, Tate Rowney, Jeremy Avigad, Prasad Tetali, Sean Welleck
In Progress
Generalized RL Pipeline for training proof optimizers for the optimization of research-level Lean theorems at scale, across metrics, and at low cost.
cLean: Verifiable GPU Programming in Lean
Riyaz Ahuja
In Progress
Framework for writing, executing, and verifying the safety and correctness of GPU programs in Lean.
Agora: Market-Based Multi-Agent Automated Mathematical Discovery
Riyaz Ahuja, Alexander Heckett, Shivansh Gour, Alexander Willoughby, Tate Rowney, Ishin Shah, Chris Su
In Progress
Market-based multi-agent mathematical discovery platform for collaborative human-AI research in formal mathematics at scale.
projects.
other.
talks.
past work.
The Purple Hand
501(c)(3) nonprofit for using data to fight human trafficking