37
$\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?

Improve this question
$\endgroup$
8
  • 6
    $\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
    Commented May 31, 2016 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
    Commented May 31, 2016 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
    Commented May 31, 2016 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
    Commented Jun 3, 2016 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
    Commented Jun 3, 2016 at 19:16

1 Answer 1

Reset to default
46
$\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

Improve this answer
$\endgroup$
2
  • 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
    Commented Jan 6, 2018 at 9:04
  • $\begingroup$ @Dap I have fixed this again. $\endgroup$
    – Neil Strickland
    Commented Jan 8, 2018 at 17:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .