dpah

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 performance 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/...

I've used Lean a fair bit (mostly contributing to mathlib), and have had a cursory glance at Coq. They are pretty similar, with really similar foundations. Both use variants of Calculus of Inductive Constructions for their foundation. Syntactically, Lean seems neater than Coq, and has more flexible pattern matching, and type inference.

It also has inbuilt support for quotient structures, which is a huge timesaver when dealing with Algebra. Might not be so important if you want to prove the correctness of programs. But I think the main advantage is that Lean is it's own meta-programming language, so you don't need to switch to Ltac/OCaml to write tactics.

The main advantage Coq has is it's code extraction feature. There was talk about implementing code extraction to C++ in Lean, but I don't think it has been done yet.

An oversimplified summary would be that Coq was designed with programmers in mind, while Lean was designed with mathematicians.

They are employing a dark pattern to make it seem that way, but it isn't so. You can just click "next" without actually entering an email. But there is no indication that the field is optional.