about.
I'm an incoming PhD student at Stanford University studying AI and formal methods under Clark Barrett. Earlier this spring, I completed my master's in Mathematics and bachelor's degrees in Mathematics and Computer Science at Carnegie Mellon University.
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 worked under Prof. Jeremy Avigad, Prof. Sean Welleck, and Prof. Prasad Tetali as 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.
Defended my Master's!
Accepted an offer to work on AWS Trainium and Neuron compiler
Accepted a PhD position at Stanford
Multi-agent theorem proving paper released
Inducted into Phi Beta Kappa
ImProver2 released
cLean milestone report released
Named as an ACS Scholar
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 2: Iteratively Self-Improving LM's for Neurosymbolic Proof Optimization
Riyaz Ahuja, Tate Rowney, Jeremy Avigad, Sean Welleck
In Submission (ICML 2026)
Generalized RL Pipeline for training proof optimizers for the optimization of research-level Lean theorems at scale, across metrics, and at low cost.
DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
Tate Rowney, Riyaz Ahuja, Jeremy Avigad, Sean Welleck
In Submission (ITP 2026)
A framework for bidirectional translation between the Lean proof assistant and external DSLs for interactive computating in formal theorem proving.
Multi-Agent Theorem Proving
Riyaz Ahuja, Shivansh Gour
Multi-agent reinforcement learning and game theory for decentralized theorem proving.
Unity: Multi-Agent Collaborative Autoformalization
Shivansh Gour, Riyaz Ahuja, Jeremy Avigad, Sean Welleck
In Progress
Multi-agent, low-cost, collaborative autoformalization platform.
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