Co-authored a Lean 4 formalization of the combinatorial framework for nilpotent orbit closure relations in classical real Lie groups, following Đoković’s work.

Code: YoungDiagram

Co-authored a Lean 4 formalization of Theorem 5.2 in Wang and Zahl’s work on sticky Kakeya sets, subsequently incorporated into a machine-checked proof of the full three-dimensional Kakeya conjecture. The formalization and its contributors were acknowledged in Guth, Wang, and Zahl’s streamlined proof.

Code: 3d-sticky-kakeya

Co-authored EdgeBench: Unveiling Scaling Laws of Learning from Real-World Environments. Contributed Lean-based evaluation infrastructure for formal mathematics, including partial-credit scoring and checks for axiom dependencies, modified theorem statements, and tampered definitions.

Paper: arXiv:2607.05155

Intern, Formal Mathematics and Forward-Deployed Engineering

• Contributed Lean/mathlib formalizations on spectral bounds, symplectic matrices, and character theory.
• Completed a formalization of the large sieve and the classical Bombieri–Vinogradov theorem.
• Developing long-horizon evaluation benchmarks.

Research Collaboration

• Contributed to Lean/mathlib, including Stacks Project tags, the Jacobson–Noether theorem, and filtered homomorphisms and exactness of associated graded sequences (#22208, #22972).
• Participated in Lean and AI for mathematics workshops, including Formalizing Class Field Theory (Oxford, 2025) and Metaprogramming in Lean 4 (Zhejiang University, 2026).

Intern, AI for Mathematics

• Developed mathematical solutions and Lean 4 formalizations in abstract algebra, category theory, and commutative algebra.
• Helped build formalized datasets for automated reasoning and theorem proving.