I am a first year master's student at New York University.
In June 2023, I graduated from the University of Chicago,
majoring in Mathematics and Computer Science.

---

Projects

EPiQC

Lambda-Q#
Mar '22 - Present. I am working with Kartik Singhal on Lambda-Q#, a formal core to Microsoft's Q#. To learn more, read the paper found at https://ks.cs.uchicago.edu/publication/q-algol/q-algol.pdf and the more recent https://ks.cs.uchicago.edu/files/thesis-proposal.pdf.

Quantum Lib
May '21 - Aug '22. I developed a linear algebra library in Coq that is currently being used by QWIRE and SQIR, two quantum programming languages. I added many proofs involving eigenvectors, invertibility, and other matrix properties. I also proved the fundamental theorem of algebra and in the process, formulated many notions from topology, calculus, and group theory, even proving Heine-Borel. I also gave a talk on the project at the 2022 Coq Workshop, part of FLoC 2022 in Haifa, Israel. My slides, abstract, and (eventually) a video recording of the talk can be found here. The actual code for the project can be found at https://github.com/inQWIRE/QuantumLib.

Gottesman Type System
Oct '20 - Jun '21. In “Gottesman Types for Quantum Programs”, Rand et al. introduces a type system, based on the Gottesman-Knill theorem for characterizing quantum circuits that use the Clifford gate set. While this system is implemented in the Coq proof assistant (allowing easy typechecking), it is not verified using that tool. This work aims to patch these holes by directly providing a semantics for Gottesman types in Coq, and proving the necessary theorems from Gottesman and Rand et al. In the process, we allow further extensions to the type system, provided that those extensions are consistent with our semantics. This allows us to verify typing rules that go beyond the limited expressivity of our current rules and the limitations of the Clifford gate set. The project can be found at https://github.com/inQWIRE/Heisenberg-Foundations. I also presented a poster at the 2021 Quantum Physics and Logic conference. The poster can be found here.

Math Research

2021 Math REU
Jun '21 - Sep '21. I spent the summer reading about algebraic geometry. With the help of my great advisor Michael Neaton, I learned a lot about the topic, reading from both Hartshorne's Algebraic Geometry and Shafarevich's Basic Algebraic Geometry. My final paper can be found at http://math.uchicago.edu/~may/REU2021/REUPapers/Zweifler.pdf.

2020 Math REU
Jun '20 - Sep '20. I spent the summer reading about elliptic curves and complex multiplication from Silverman and Tate's Rational Points on Elliptic Curves. My final paper can be found at http://math.uchicago.edu/~may/REU2020/REUPapers/Zweifler.pdf.

Personal Projects

Spinning Shapes
Owen Fahey and I have been working on various graphics projects using p5.js and Three.js. One preliminary project can be found here. Expect more to come.