I will describe how the Lean proof assistant software can be used to teach mathematical reasoning to young students at university. This is different from teaching how to use Lean. Here Lean is only a tool, not the end goal.

I will explain what we can hope to teach using this tool, what are the available resources for teachers, and what choices should be made. I will then show my teaching library, Verbose Lean, which uses controlled natural language and customizable automation to optimize transfer of skills to paper proofs.