[FOM] formal proofs

[David Roberts]

Dear Freek,

why would you try to emulate HoTT in a membership-based foundations?
Why not just prove B-M using the usual textbook approach or better yet
in some computer formalised ZFC, since that is apparently the
gold-standard. (Harvey Friedman can pick his favourite proof
assistant, if he likes, perhaps one in which he has had some
nontrivial input)

As far as models go, you'd better use simplicial sets - the cubical
sets version is in-development; I don't know its exact status. It is
aimed as giving a computational interpretation of HoTT, anyway, not
just a model.

Regarding person-years spent on formal computer proofs in HoTT, I gave
a very rough upper bound in one of my previous emails: 21 people have
contributed to the HoTT repository on Github, though a number of them
are only a handful of edits. This is to date, rather than at the
2-year mark by which time B-M had been formalised. Looking back, there
are 10 people who contributed more than 10 lines of code from the
start date to the beginning of May in 2013 (seven of which contributed
1000 lines of code or more). I would disallow your putative PhD
student from accessing the libraries in existence (in Mizar, say),
since this little team I assume did not have any pre-existing HoTT
libraries.

Best regards,

David



On 23 October 2014 20:51, Freek Wiedijk <freek at cs.ru.nl> wrote:
> Dear Tim,
>
>>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?
>
> I would guess that if one really would do this, still the
> HoTT formalization would be much shorter.  So I think it
> still would be taken as a reason to claim HoTT is much
> better than the traditional way of working.
>
> So one would really need to separate the formalization into
> two parts: one part in which one formalizes the lemmas and
> proof principles that in HoTT one gets for free.  And then
> a second _very separate_ part, which would be a proof of
> this Blakers-Massey theorem.  To make it a fair comparison.
>
> Another question for Urs: if I were to formalize a model
> of HoTT (cubical sets, is that a model for HoTT?) in a
> traditional framework, and then just glue the Agda proof on
> top of that, would that count as a refutation of the claim?
>
> Also, I would like to understand the models of HoTT better.
> If I just interpret the types as topological spaces and the
> equalities as the existence of paths, do I get a model of
> HoTT?  If not, why the the claim that HoTT is about homotopy
> theory?  But if so, why all the fuzz about the cubical sets?
>
> Freek
> _______________________________________________
> 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