Formalization on Lie Algebra Representation Introduction This is an experimental formalization project for BICMR seminar. We generally formalize contents in Introduction to Lie Algebra and Representation, Chapter 1. Final goal for this project is to prove Weyl's theorem.