Yes, the stack of papers at my desk with random scribbles are a far cry from a verified proof written in lean. There is lots behind a proof that you don't neces

Yes, the stack of papers at my desk with random scribbles are a far cry from a verified proof written in lean. There is lots behind a proof that you don't necessarily see reflected in a piece of code/proof. So I agree, something formal is like a final step.