I became fascinated by Lean last week while watching Terrence Tao stream his proof work on Youtube. At least on the surface his thought process and workflow looked very similar to what I do in my IDE when programming, especially when coding in a very strongly typed language like Scala with FP style.
If I can work through math proofs in an IDE with Lean helping check my work I might finally get around to diving into the higher level math I’ve always wanted to. Could open some doors to us working folks that don’t have an instructor to review our proof attempts.