Programming

I’m interested in programming (Python, Lean, SageMath, etc) and contributing to open sources. You can find some of my projects and contributions below.

Lean

• Sphere Packing (Maintainer, with S. Hariharan, C. Birkbeck, B. Mehta, M. Viazovska)
  • Formalizing Viazovska’s proof of the sphere packing problem in dimension 8
  • There was a recent breakthrough by Math Inc.’s Gauss, producing sorry-free proof of dimension 8 and 24 sphere packings. See Math Inc.’s press release, Lean Community Blog 1, IEEE Spectrum article, NYT article.
• Mason-Stothers and Polynomial ABC (with J. Baek)
  • Formalize Mason-Stothers theorem and polynomial ABC conjecture
• Formal Conjectures (Contributor, by Google Deepmind)
• mathlib4 (Contributor, by Lean Community)
• Lean-GAP (paper)
  • Formalizing exercises in Dummit-Foote’s Abstract Algebra book

SageMath

• Positive quasimodular forms
  • Sage implementation related to my research on quasimodular forms
• Machine learning number fields
  • Sage implementation of the paper, “Machines Learn Number Fields, But How? The Case of Galois Groups” with K. Lee.
• Function field
  • Sage implementation related to my research on function fields
• Bhargava cube
• Quantum modular form
• Number theory tutorial
  • tutorial lecture for Math254A at Berkeley
• Murmuration

Miscs

• awesome-ai-for-math (Maintainer)
  • List of papers on AI for mathematics
• Erdős Problems + OEIS (Contributor, by Terence Tao)
• Knowledge Tracing in PyTorch (archived)