[comnetxr]

has anybody proved something interesting in Lean? Perhaps not too difficult, but some proposition that might take a couple of days of work done in hours? I'm all for encoding foundations in a programmatic framework, but it seems that the idea here is to make this a useful tool for practicing mathematicians. The documentation didn't seem to have any examples of how that might happen.

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

[agentultra]

It's also a useful tool for practising programmers as well!

The documentation for it isn't so great but Lean is a fully dependently typed programming language with a good VM. It is optimized for interactive theorem proving which means the type checker is really fast. I think getting a good native compiler out of it is not far off.