Questions on proof assistants

[Mario Carneiro]

I agree with most of Buzzard's remarks, I just have some minor
clarifications on the proof of Dirichlet's theorem in lean via wholescale
translation from Metamath.

On Wed, May 13, 2020 at 9:44 PM Buzzard, Kevin M <k.buzzard at imperial.ac.uk>
wrote:

> 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.
>

The original source text, metamath's set.mm database, is about 30 megabytes
of mixed human source text and compiled proofs. These proofs are translated
quite directly to lean, and blowup is minimal. Because the proof of
Dirichlet does not use the entirety of the library, only about 18 megabytes
(200,000 source lines) are needed, roughly the first half of the library.
(This theorem was targeted because it is relatively simple to interpret in
type theory, yet has many nontrivial dependencies.)

The code is not incomprehensible. In order to make sure lean doesn't
misinterpret the file, it is deliberately printed in lean's most verbose
mode, but the only thing between this and a readable source is a good
pretty printer and declared notations. The final stage of the proof is
"alignment", taking the now-proven theorems about a model of ZFC inside
lean and translating the metamath notions to lean notions, and this went as
smoothly as it is reasonable to expect.


> 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.
>

This is almost certainly false. While I think it is much more likely for a
lean statement in metamath to be incomprehensible as a result of the great
number of implicit arguments, I don't believe there will be any technical
problems with the translation; that is, I believe it is feasible to check
all of lean's mathlib after translation to MM0 or metamath, most likely in
much less time than the original compile.

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.
>

While I think I know what you mean by this, I disagree. It is certainly
possible to get the 18 megabyte proof to the same level of readability as a
metamath proof, because it is a metamath proof, suitably dressed up. As to
whether we can get beyond metamath level readability (which is still quite
baroque) to something more like a regular mathematics paper, I am hopeful.
Some things are easy, like using conventional mathematical notations for
symbols, while other things are harder, like finding "key" steps in the
proof, hiding basic propositional logic manipulations, and minimizing the
amount of repeated wording. But I see no reason to believe that improving
readability of formal proofs is an insurmountable problem, although it is a
vaguely defined one. I think machine learning techniques have already shown
promise in many similar areas, both in generating proofs and in producing
human language, such that this "informalization" task would seem to be
within reach. Certainly just adding comments to code is an easier solution,
but it is much less likely to survive a wholescale translation unless the
comments themselves are tracked.

Note that the metamath set.mm database is written by humans, not machines.
The calculus may well be different if one tries to apply these same
techniques to genuinely computer-written proofs, because then one cannot
simply structure the output around human patterns in the data. Computer
proofs often have much stronger patterns, but they may not lend themselves
well to display purposes.

Mario Carneiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200513/044722d9/attachment-0001.html>