That's a vague question so allow me to tighten it up a bit.

I recently noticed that there is a formal machine verified proof of the Central Limit Theorem (CLT) implemented with Isabelle. This requires a substantial amount of machinery that is taught in undergraduate courses on calculus, measure theory and probability theory. As Williams' textbook *Probability with Martingales* culminates with CLT it seems like it might be fair to conservatively estimate that maybe half of an undergraduate level probability theory course has been formalised.

So would it be fair to say that half of the material (in general) that is taught to mathematics undergraduates has been formally verified by machine? If not, what similar proposition is true?

Formal Proof--Getting Startedfrom a special issue of Notices on formal proof. $\endgroup$2more comments