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?
Best Answer
A couple of years ago I made a database of all the formalization files that I could find at that point, in several different systems. You can view it here:
http://bim.shef.ac.uk/formal/list_formalizations.php
I would guess that the proportion of a typical undergraduate curriculum that has been formalized in at least one framework is substantially greater than 50%. However, the general usability of these systems remains poor. Even in a single proof assistant, there are problems with incompatible versions, incompatible libraries and incompatible approaches to the same mathematical material in a single library, and various kinds of bitrot. Documentation is often poor. Typically it is aimed at people who are primarily interested in the technology of proof assistants, and if not, then it is aimed at people who already know the relevant mathematics very well. I once gave a talk about this sort of thing. The slides are here:
http://neil-strickland.staff.shef.ac.uk/talks/pa_talk.pdf
and there is video here:
https://www.youtube.com/watch?v=4O84o1hk1Qs