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.