Formalizing Coxeter Group, Hecke Algebra, and Kazhdan-Lusztig Theory in Lean

Welcome to our project, where we are dedicated to formalizing the Coxeter Groups, Hecke Algebra, and Kazhdan-Lusztig theory using the Lean theorem prover. Our mission is to bridge the gap between abstract mathematical concepts and their practical implementation in computer-assisted proofs, enhancing both the accessibility of these theories.

About the Project

The project aims to:

  • Formalize the foundational aspects of Coxeter Groups, and Hecke Algebra.

  • Implement the Kazhdan-Lusztig algorithm in Lean.

About Our Team

Our project is powered by an international team of dedicated students from Xiamen University, the National University of Singapore (NUS), and Renmin University.

Get Involved

Check out our project on Gitee at Coxeter4 to see where you can help. Whether it’s through coding, documentation, or testing, your contributions are invaluable to our progress.