I am a PhD student at UT Austin, working in the Trustworthy and Intelligent Systems Lab (Trishul) under Swarat Chaudhuri. I am interested in developing intelligent systems for mathematics and other scientific domains. Previously I have worked on number theory of quadratic forms, and single-cell computational genomics.

Currently, I am interested in understanding how AI can integrate well into real workflows of mathematicians and scientists. Recently, we published our work on improving both the best known lower and upper bounds on the Grothendieck constant (see here), together with a companion case study on the human-AI research process behind it (see here). This endeavor was made possible through collaboration between mathematicians and AI systems. I feel hopeful that scientific advances will be made possible in the near future through proper deployment of these tools when useful. If you are interested in my thoughts on AI for discovery, please reach out!

NEWS

• Two new companion papers on the Grothendieck constant are out. The first tightens the best known bounds to \(\frac{6\pi}{11} \leq K_G \leq \frac{\pi}{2 \log(1 + \sqrt{2})} - 10^{-4}\), determining the previously unknown tenths digit of \(K_G\) to be 7 (read it here). The second is a detailed case study of the long-horizon AI research system we built to find these results, and of what worked and what did not in collaborating with it (read it here).
• Our paper on improving the upper bound on the Grothendieck constant via AI guided search is now out. This improves upon the previous best known explicit bound from 1979. Read the paper here.
• Our paper on automatic theory discovery received Spotlight at NeurIPS 2025. This work introduces an RL environment that models theory discovery, and explores the problem of learning interestingness. Read the paper here.

PAPERS

Find more info on these papers as well as other publications here.

1. New Lower and Upper Bounds for the Grothendieck Constant, Rahul Saha*, Alan Li*, Anton Xue, Swarat Chaudhuri, Adam Klivans, Pravesh K Kothari, Raghu Meka
2. Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human-AI Mathematical Collaboration, Alan Li*, Rahul Saha*, Anton Xue, Swarat Chaudhuri, Adam Klivans, Pravesh K Kothari, Raghu Meka
3. The Grothendieck Constant is Less Than \(\frac{\pi}{2 \log(1 + \sqrt{2})} - 10^{-5}\), Alan Li, Rahul Saha, Anton Xue, Swarat Chaudhuri, Adam Klivans, Pravesh K Kothari, Raghu Meka
4. Learning Interestingness in Automated Mathematical Theory Formation, George Tsoukalas, Rahul Saha, Amitayush Thakur, Sabrina Reguyal, Swarat Chaudhuri
5. On three-term linear relations of theta series of positive-definite binary quadratic forms, Rahul Saha, Jonathan Hanke
6. LLMSTEP: LLM Proofstep Suggestions in Lean (NeurIPS 2023 Math AI ), Sean Welleck, Rahul Saha
7. A New Approach towards Autoformalization, Nilay Patel, Rahul Saha, Jeffrey Flanigan
8. Engineering mtDNA Deletions by Reconstructing End-Joining in Human Mitochondria, Yi Fu, Max Land, Ruobing Cui, Tamar Kavlashvili, Minsoo Kim, Toby Lieber, Keun Woo Ryu, Emily DeBitetto, Ignas Masilionis, Rahul Saha, Meril Takizawa, Daphne Baker, Marco Tigano, Ed Reznik, Roshan Sharma, Ronan Chaligne, Craig B Thompson, Dana Pe’er, Agnel Sfeir

RESEARCH INTERESTS

How did complex mathematical ability arise from millions of years of evolution? How are humans capable of discovering relativity, or proving the 290 theorem? From both cognitive and mathematical perspectives, this is a very compelling question to me. For my doctoral research, I want to study this problem from the angle of automatic theorem proving, discovery, and the design of AI tools that mathematicians can actually use.

• Automatic Theorem Proving. How do we train agents to rigorously prove mathematical statements? The stepwise tactic prediction and tree search that defined this area a few years ago has largely given way to models that reason at length and emit whole proofs, trained with reinforcement learning against a proof checker. That shift moved the hard questions rather than settling them: formal corpora are still small relative to what training wants, credit assignment over a long proof attempt is still crude, and the strongest natural-language reasoning is still only loosely connected to anything a verifier will accept.
• Automatic Discovery. How do humans come up with newer concepts in mathematics and science? This is a generative AI problem but the twist is that the space is highly discrete.
• AI for Long-Horizon Research. Real research problems are open-ended and unfold over weeks or months, not over a single query. What has to be true of an AI system before it can make progress on that timescale — carrying context across a long effort, recognizing which of its own directions are worth continuing, and knowing when to hand the problem back to a human? Our work on the Grothendieck constant was an attempt to find out by actually running such a system on an open problem.

APPLICATIONS

I believe that the fruits of my research will empower us to discover newer frontiers of science, empower mathematicians with the ability to ask and answer deeper questions, boost productivity of scientists, and help humanity towards solving some of the hardest problems.

PORTFOLIO

My projects are listed here. Some of these projects are no longer maintained, but I am happy to entertain any questions or comments.