Research projects

Integrated Explicit Analytic Number Theory Network

Dec 2025 – present

PIs: Terence Tao, Ernest K. Ryu, Dima Shlyakhtenko

  • Build agentic systems to integrate and maintain explicit analytic number theory results within a formal Lean network, with automated propagation of updates when upstream theorems change (repo).

UCLA Moonshot

Apr 2026 – present
  • Co-led development of the UCLA Moonshot Harness for agentic proof search. Participated in the First Proof Second Batch Challenge (code).
  • Built a follow-up harness for math paper verification (code, website).