34
$\begingroup$

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?

$\endgroup$
  • 5
    $\begingroup$ It might be fair, but I don't think it is correct. You may look over the Archive of proofs that the Isabelle site maintains, as well as review the ArXiv paper you mention. My guess is that the proofs are optimized for verification and not for pedagogy, and that the actual theorems you will see (except for the conclusion) will not be structured or represent much material from any course outside that of automated theorem proving. Gerhard "Won't Formally Prove My Guess" Paseman, 2016.05.30. $\endgroup$ – Gerhard Paseman May 31 '16 at 0:32
  • $\begingroup$ The paper I linked to does list a number of standard theorems from an undergraduate course that were proved among the way. I can't yet read Isabelle well enough to know how close the statements of these theorems are to the usual versions. $\endgroup$ – Dan Piponi May 31 '16 at 0:44
  • 6
    $\begingroup$ You can check the list of theorems proved in Mizar. Another list of theorems with formalized proof can be found here. It is based on the paper Wiedijk, Freek: Formal Proof--Getting Started from a special issue of Notices on formal proof. $\endgroup$ – Martin Sleziak May 31 '16 at 2:32
  • $\begingroup$ Can you come up with a more quantifiable measure? One way is to compare the byte sizes of: 1) some corpus of existing formalized theorems (that have been proven) 2) some corpus of existing UG texts (or just theorem statements). You need to specify the corpora more exactly though (this ignores the problem if judging if a particular UG theorem has been truly formalized, just if a formalized proof corresponds to UG. math. Even then my guess of this is that the ratio will be tiny. $\endgroup$ – Mitch Jun 3 '16 at 19:15
  • $\begingroup$ Frankly, if you take some well understood subset of math, like Euclid's elements, which is conceptually provable entirely by Groebner Bases, only very few of those theorems have explicit formalized versions (with supporting computer proofs). $\endgroup$ – Mitch Jun 3 '16 at 19:16
45
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ bim.shef.ac.uk/formal/list_formalizations.php is giving an error agin (Access denied for user 'pm6maths_formal'@'localhost'). And it has a robots.txt stopping it from getting archived on archive.org or Google's cache. $\endgroup$ – Dap Jan 6 '18 at 9:04
  • $\begingroup$ @Dap I have fixed this again. $\endgroup$ – Neil Strickland Jan 8 '18 at 17:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.