I contribute to collaborative projects that develop mathematical knowledge bases and formal proofs in Lean.
EconCSLib
A Lean 4 library and knowledge base for computational economics, built on Mathlib. It develops reusable foundations for game theory, auctions and mechanism design, social choice, fair division, and matching.
Code · API documentation · Knowledge blueprint
LanglandsProject
A knowledge base for the Langlands program, paired with a growing Lean 4 library. The project connects definitions, results, and proofs with their formal counterparts, starting with algebraic groups, homogeneous spaces, and related representation theory.
Coxeter Groups, Hecke Algebras, and Kazhdan–Lusztig Theory
This project aims to formalize foundational results on Coxeter groups and Hecke algebras and implement the Kazhdan–Lusztig algorithm in Lean.
The team includes students from Xiamen University, the National University of Singapore, and Renmin University. Contributions to formalization, documentation, and testing are welcome.