DPdpah·Sep 30, 2019
Well, there is the entire mathematical components library[0]. It's still fairly elementary, roughly at an advanced undergraduate level.
Right now it actually takes far more time to write lean code than to prove things by hand. What is typically done in a single lecture in an intro Algebraic Number Theory course can take hours upon hours to implement. E.g. the Pell equation [1]. You have to be extremely explicit about everything, and can't handwave the details you do in human proofs.
Right now the overhead of writing proofs in Lean is so large that you'd prove a theorem with pen and paper before attempting it in Lean. So far it is a useful tool for proof verification, but not for actually coming up with them.
As things stand, computer proofs are only better than humans for things that are highly combinatorial in nature. which due to perfor
Read the rest
mance concerns usually aren't written in languages running in VMs.
[0]https://github.com/leanprover-community/mathlib
[1]https://github.com/leanprover-community/mathlib/blob/master/...