Thanks for the insight on this, by the way; I'm more of an applied math person, so I have no firsthand experience of things like computer-verified proofs, Coq,

Thanks for the insight on this, by the way; I'm more of an applied math person, so I have no firsthand experience of things like computer-verified proofs, Coq, etc. What do you think are the specific ways in which a proof compiler would be different?