Yes! I’m not suggesting they are synonymous, but proofs in coq are definitely formal proofs (as I understand that term/phrase).