Comment by nodogoto

> Lean to me is not only obscure but unapproachable by someone from a non-mathematical background. ... If we want to democratise formal methods and theorem proving ...

For whom is that a goal? Are there really that many individuals at the intersection of "I need to use a theorem prover" and "I don't have formal mathematical training"?