Lean as a proof assistant for students

Stream: new members

[Samuel Levi Schmidt]

Hello,

my question is mainly targeted towards (math) students*:

Do you actually use Lean in your studies if you have to proof something?
If not, why?
If yes, how is the experience?

When I first read about "proof assistants" I imagined a program that would, well, assist users in various ways with writing proofs.
My impression now is that the focus of Lean is to formalize mathematics?

*of course, anyone can comment :D

[Dan Velleman]

Many users of Lean are focused on formalizing mathematics. But there are also people who are interested in using Lean in education. For information about that, you might want to look here: https://leanprover-community.github.io/teaching/index.html

[David Loeffler]

My understanding is that "proof assistants" are so called because they assist you in explaining the proof to the computer, not because they assist you in understanding it yourself.

A proof assistant can be useful to help a human understand a proof, but only in the sense that a carpenter's spirit level is useful in building a house: it will show you when and where you have got something wrong. It won't fix the mistake for you.