Lean语言的目标是形式化表达无歧义的可机械验证的数学。但是作为一种程序语言，Lean距离日常语言尚有距离……or not?
kevin buzzard等人已经在尝试以Lean做本科生入门数学的途径。我希望在本项目中更加进一步地证明这一点，我决定尝试完全用Lean语言写一部本科生数学教材。这听上去非常Bourbaki（x）……
本项目目前是Lean community官方教程mathematics in lean的中文译本，未来希望发展得更完备一点。
电子书请见 https://redblack23.github.io/mathematics_in_lean_zhCN
祝读者学习愉快！