Curriculum Vitae [cv]

Seeking Research Opportunities

Open Source Project. Kodama, A Typst-friendly static Zettelkästen site generator. Inspired by Jon Sterling’s Forester. In January 19, 2025 - $\infty$.

Lecture Note. “A Correspondence between Stack Permutations and Binary Trees via Hille Encoding” In December 10, 2025.

Lecture Note. “A Brief Survey of UMAP”. In November 9, 2024.

Competitive Programming. Codewars Rank 2 kyu. Top 1.659%. In October 2024.

Conference Participant. Workshop on Formal Proofs and Lean. In National University of Singapore, The Institute for Mathematical Sciences, Apr 15, 2024 - Apr 26, 2024.

Mini-Course Participant. Algebraic $K$-Theory and Prismatic Cohomology. Longke Tang. In Beijing International Center for Mathematical Research, December 12, 2023 - January 3, 2024.

Visiting Scholar. The integration of Lean4 theorem prover with large language models. Peking University. In Beijing International Center for Mathematical Research, November 2023 - September 2024. Related Projects & Papers: “Herald: A Natural Language Annotated Lean 4 Dataset”, Powered by jixia, A static analysis tool for Lean 4. “A Semantic Search Engine for Mathlib4”, Powered by LeanSearch, A semantic search engine for Lean 4 projects.

Acknowledged Contributor. “EgoLocate: Real-time Motion Capture, Localization, and Mapping with Sparse Body-mounted Sensors”. In ACM SIGGRAPH 2023.