[FOM] unintelligible proofs

[José Manuel Rodriguez Caballero]

>
> David wrote:
> A proof of the RH [Riemann hypothesis] of which we do not understand
> anything,

other than the fact that it
> is correct (as witnessed by some computerized proof checker) will probably
> not be very valuable (cf. the proof of the four colour theorem).


There are mathematical papers assuming that RH is true and there are
mathematical papers assuming that RH is false. To know in some way which
one is the case will allow us to make progress just in one direction until
the proof of RH will be understood.

Your answer was motivated by my comment on proof assistants. So, I will
bring an example of how intelligible current proofs assistants are. In
Isabelle/HOL there is a language, called ISAR, which allow you to write
proofs in an intelligible way, just as in any informal mathematical text.
People can understand a proof in a printed text written in ISAR as if there
where looking at the computer. As far as I know, this is not possible in
Coq, because Coq lacks its own version of ISAR.  Here is the reference to
ISAR: http://isabelle.in.tum.de/doc/isar-ref.pdf

You could read the proof of theorem 26 in my preprint:
https://arxiv.org/pdf/1709.09617.pdf

and its implementation in Isabelle/HOL, using ISAR:
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory/blob/master/TwoDenselyDivisible.thy

Which one is the most intelligible, the one from the text or the one from
the proof assistant?

I think that we all agree that the version written in ISAR is easier than
the one in
my original manuscript, because the computer forced me to write all the
details. To check a theorem in a proof assistant before the publication is
a nice way to accelerate the reviewing process (Voevodsky's dream). If
there are glaring inconsistencies in a particular theory, after its
formalization in a proof assistant, the editor can derive a contradiction
in the proof assistant. The inconsistency may be found using an automatic
generator of counterexamples known as nitpick:
http://isabelle.in.tum.de/dist/doc/nitpick.pdf

Kind Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180901/e99c2332/attachment.html>