Yes, and the problem of deciding which lemmas to prove and in general what structure to try for a proof is also far from begin formal. Verifying a proposed proof is the formal bit.
Yes, and the problem of deciding which lemmas to prove and in general what structure to try for a proof is also far from begin formal. Verifying a proposed proof is the formal bit.