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
• DifferentProofs
  • Formalizing different proofs of the same theorems.
• cohn-elkies-refactor
  • Refactored version of OpenAI’s formalization on their result on Cohn-Elkies linear programming bound and the sign uncertainty principle. It also proves missing results in the original report, and follow the original proof rather than the slightly different proof in their formalization. See blog for the details.

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
• TeX-puzzles
  • Latex packages for 12 permutation puzzles beyond Rubik’s cube
• Erdős Problems + OEIS (Contributor, by Terence Tao)
• Knowledge Tracing in PyTorch (archived)