Home
I am a Formal Verification Engineer at Intel Corporation.
In August 2022, I completed my Ph.D. in Mathematics at the University of Pittsburgh, where I was advised by Tom Hales.
Research Interests
My research interests are in Discrete Geometry, Optimal Control Theory and Formal Verification. I also hold a Certificate in Quantitative Finance.
Internships
- Oracle Labs from May-July 2019.
- MIT-IBM Watson AI Lab from July-September 2020.
Books
-
"Packings of Smooth Polygons" (with Thomas Hales): This book studies the Reinhardt problem in Discrete Geometry by reformulating it as a problem in Optimal Control Theory. Using this framework, we prove that the minimizer of this problem is a smoothed polygon, which settles a 1947 conjecture of Kurt Mahler.
This research has been featured in Quanta Magazine and the German newspaper Süddeutsche Zeitung.
Papers
- "On the Reinhardt Conjecture and Formal Foundations of Optimal Control" (Ph.D. Thesis)
- “Formalization of a Stochastic Approximation Theorem” (with Barry Trager, Avi Shinnar and Vasily Pestun) Accepted to ITP 2022
- “CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq” (with Avi Shinnar, Barry Trager, Vasily Pestun and Nathan Fulton) Accepted to CPP 2021
- “A Formal Proof of PAC Learnability for Decision Stumps” (with Joseph Tassarotti, Anindya Banerjee and Jean-Baptiste Tristan) Accepted to CPP 2021
- “On Pythagorean Triples of the Form (i,i + 1,k)” in Resonance: Journal of Science Education,September 2009, Volume 15, Number 09.
- “On a Definite Integral of the Fractional Part Function” in Resonance: Journal of Science Education,May 2012, Volume 17, Number 05.
You can find more in the things I've written.