Comment by Almondsetat

>Lean doesn't solve the problem of verifying that a formal theorem actually states what we think it states rather than something else.

With all honesty, if a tool existed that did that we would have solved maths. Or at least we would have solved human communication. In both cases it would be the most studied thing in the world, so I don't know where this belief would come from