Questions on proof assistants

[Buzzard, Kevin M]

> I see on Freek Wiedijk’s page
>
> http://www.cs.ru.nl/F.Wiedijk/100/index.html
>
> that proof assistants are doing reasonably well at formalizing the “top 100” theorems:
>
> HOL Light 86
> Isabelle 83
> Metamath 74
> Coq 70
> Mizar 69
>
> My questions are:
> 1) which of these can make use of work done in which other ones?
> 2) which of these would be the easiest for mathematicians with some programming experience to learn to use to create machine-verifiable proofs?
> 3) which of these have a good translator that turns a machine-readable proof into something a human reader might gain insight from?
>
> — JS

For Q1, rather than answering it, I will ask an analogous question. Consider the programming languages Python, C++, Java and Haskell. Which of these can make use of work done in which other ones? The answer is that, unfortunately, this is not the right question. Each language has its own way of doing things and even if one wrote some computer program which translated basic code written in one language to another, one would end up with inefficient code which does things in the "wrong way". Can one deduce anything about the relative merits of Python, C++, Java and Haskell from this state of affairs? Each is good at what they're good at.

Perhaps I will comment that a program called metamath0 https://github.com/digama0/mm0, written by Mario Carneiro, did actually translate Dirichlet's proof of infinitude of primes in an arithmetic progression from Metamath into Lean; it ended up as 18 megabytes of incomprehensible computer-generated code, but it compiled. It would be essentially impossible to write code which went the other way and actually worked in practice on reasonable examples though, I suspect, for the same sort of reasons in the previous paragraph.

For Q2, I think that a few years ago none of them were easy. I have spent a lot of time over the last few years of my life trying to make Lean easier for mathematicians (and in particular mathematicians like geometers, topologists or number theorists with no background in foundations) to use. I wrote a game: http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ which is very popular with mathematics undergraduates, I formalised the problem sheets I was giving out to students https://github.com/ImperialCollegeLondon/M40001_lean and run a club where I teach them to use Lean to answer them, and I am one of many people trying to formalise an entire undergraduate mathematics curriculum in Lean: see an overview here https://leanprover-community.github.io/mathlib-overview.html of how far we have got. Note that actually I am concentrating more on undergraduates than staff, because I believe that the inevitable paradigm shift will occur only when these systems are commonly used by the undergraduate community rather than when researchers are trying to use them. Also we are not concentrating on Freek's list, we are concentrating on the kind of mathematics which mathematicians do in 2020, from undergraduates to professionals. As for higher level proofs, the sensitivity conjecture proof https://www.quantamagazine.org/mathematician-solves-computer-science-conjecture-in-two-pages-20190725/ was formalised in Lean https://github.com/leanprover-community/mathlib/blob/3f216bc6a2c3729391ca1c8aaaf156fc96e7f10e/archive/sensitivity.lean#L389-L390 , the Ellenberg-Gijswijt Annals paper https://annals.math.princeton.edu/2017/185-1/p08 has been formalised in Lean https://lean-forward.github.io/e-g/ and so on, all within the last few years (Lean has only existed since 2013). A few months ago it was pointed out that no theorem prover had formalised the proof that you can't chop a cube up into finitely many smaller cubes all of different sizes (this is a question on Freek's list), and within a few days Floris van Doorn had formalised that proof in Lean https://github.com/leanprover-community/mathlib/blob/master/archive/cubing_a_cube.lean . That event, and the fact that some modern non-foundational mathematics can be formalised in Lean by experts without too much trouble, made me conclude that probably in theory most of the items on Freek's list can be formalised in Lean (other than FLT, which is a $100,000,000 grant away which nobody will fund because nobody cares).

3) Nothing can translate Carneiro's 18 megabyte proof of Dirichlet into human-readable form. However there is nothing stopping humans from writing well-documented code which other humans can read. Take a look at Patrick Massot's Lean tutorial project, for example https://github.com/leanprover-community/tutorials/blob/master/src/exercises/05_sequence_limits.lean . Note however that these are proofs and exercises written by humans, for humans. I don't think anything can translate some gigantic abstract graph of types and terms into something a human can comprehend.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200513/63d5beb8/attachment-0001.html>