Comment by cv5005

Maybe a naive question, but how does one know that a particular lean proof is actually a proof of what one thinks? Like, ok the logic checks out and it proves something, but there's still the problem of does this logical result actually prove the initial question that was asked?