[FOM] formal proofs

[David Roberts]

Hi Tim,

Urs was not exactly precise in what you call his gauntlet. Let me be
more so. The Mizar Mathematical Library is

"one of the leading approximations to the QED utopia of encoding all
core mathematics in computer verifiable form." (Wikipedia, citing
Freek Wiedijk in
http://logika.uwb.edu.pl/studies/index.php?page=search&vol=23)

Mizar is based on Tarski-Grothendieck set theory, so a reasonable
approximation for ZFC, or at least much closer than Coq's CoC/MLTT. In
Mizar, "more than 10,000 formal definitions of mathematical objects
and about 52,000 theorems proved on these objects. More than 180 named
mathematical facts have so benefited from formal codification. [1]"
(Wikipedia again)

[1] http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename=mml-facts.mqt&argument=number+102

Searching for the word 'homotopy' at http://mmlquery.mizar.org/, I get
no results. Scanning the list [1] of named theorems I get no homotopy
theory related results. So let us say Mizar is starting from a blank
page as far as homotopy theory goes, though there is an active
community that has a working familiarity with how to prove things in
Mizar, and there is about 40 years of development.

Now HoTT/Coq only got started a few years back, certainly no more than
four years in a serious way. The homotopy type theory Github
repository for code started on Mar 20, 2011. I don't know the exact
date the B-M theorem was proved, but it was mentioned in a blog post
on 20 May 2013. So just over two years from scratch to proving,
formally, the Blakers-Massey theorem. Others may be able to whittle
down that time, so let us make it a round two years.

Here is the concrete challenge:

- Can the Mizar community give a formal proof of B-M, starting today,
in two years' time?

However! The Coq proof does not just prove B-M for topological spaces,
but in all (infinity,1)-toposes. Thus if one wanted to compare
like-for-like, the Mizar community would have to prove it for all
(infinity,1)-toposes. The relevant source material is Jacob Lurie's
1000-page book 'Higher Topos Theory'.

At one page a week, according to the recently given estimate, we are
looking at a lot of work to get it done. I would allow the Mizar
community the same number of mathematicians and computer scientists as
the HoTT project had over those two years. The homotopy type theory
book lists approx 60 names as participating in the special year
program as IAS, full-time and on a visiting basis, so this is an
estimate of the number of people who could have helped, directly or
indirectly, with the formal proof of B-M. In reality, it was far fewer
who actually wrote the code (the Githib repository lists 21 people who
contributed code). Note that the Coq proof did *not* proceed by
formalising Lurie's book, which is written in such a way that it can
be taken to be founded in ZFC + possible universes.

If the Mizar community, or any other formal proof community, could
prove this theorem formally in two years, I for one would tip my hat
to them, and reconsider my position, which is the same as Urs', that
traditional membership-based formal systems make for impractical
formalised proofs.

Cheers,

David


On 22 October 2014 06:47, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> Urs Schreiber wrote:
>
>> A good example of this is the formal proof, in HoTT, of the
>> Blakers-Massy theorem
>> (http://ncatlab.org/nlab/show/Blakers-Massey+theorem) by Lumsdaine,
>> Finster and Licata. The full formalization is here:
>>
>>
>> https://github.com/dlicata335/hott-agda/blob/master/homotopy/BlakersMassey.agda
>>
>> I'd think that with traditional foundations even stating this theorem
>> formally is impossible for all practical purposes, let alone formally
>> checking its proof.
>
>
> This is a nice gauntlet!  Before a traditionalist embarks on a project to
> refute this claim, let me clarify what is at stake.
>
> Question for Urs: Suppose a traditionalist were to thoroughly refute your
> claim above.  Would that "score any points" for the traditional side in this
> debate?  Or is this just a casual remark on your part, which if refuted
> would not cause you to change your mind on any substantive issue?
>
> Tim
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom



-- 
Dr David Roberts
Research Associate
School of Mathematical Sciences
University of Adelaide
SA 5005
AUSTRALIA