M40001_lean reviews and mentions

• A New Crisis in Mathematics?
  1 project | /r/math | 25 Jan 2022

  Somewhat orthogonal, I think what Imperial College London is doing in their undergraduate introductory mathematics course -- teaching Lean to freshmen (who are interested) -- is highly interesting. It took me until my 3rd or 4th semester until I properly understood how to write a proof. Having taken a class on interactive theorem provers in my 4th semester definitely helped this. The fact that the computer immediately tells you that your proof is correct is really nice, and really helps you learn. Also, the computer showing you the current proof state and freeing you from juggling with all the assumptions in your head teaches you how to do this and shows you which operations on your assumptions are possible.

• Propositional logic exercises with the lean theorem prover
  1 project | news.ycombinator.com | 21 Oct 2021