[FOM] formal proofs

[Bas Spitters]

Dear Tim,

A short remark. Feit-Thompson was proved in the calculus of inductive
constructions (Coq) and Flyspeck used HOL.
Neither of them used ZFC and computation was very important in both theorems.
This is in line with the development in HoTT.

Bas

On Mon, Oct 27, 2014 at 1:56 AM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> Dominic Mulligan wrote:
>
>> Hmm.  Paraphrased, isn't "Roberts' Gauntlet" asking a group of people with
>> no interest of particular expertise in the subject of homotopy theory (Mizar
>> users, who as Roberts points out, in 40 years of continuous development of
>> the tool have not once aimed to formalise homotopy theory --- giving as good
>> an indication as any to where their interests and knowledge lie) to compete
>> in a timed race against experts in the field in formalising a major result?
>> This is being interpreted as a serious challenge and something we can draw
>> conclusions from ... why exactly?
>
>
> I was the one who introduced the word "gauntlet", so perhaps I can comment.
>
> Recall that Urs Schreiber originally stated, "I'd think that with
> traditional foundations even stating this theorem [Blakers-Massey] formally
> is impossible for all practical purposes, let alone formally checking its
> proof."  David Roberts afterwards strengthened the challenge from
> "impossible for all practical purposes" to "impossible in two years," and I
> agree that raising the bar that high makes the challenge less interesting.
> Let me stick to Schreiber's form of the challenge.
>
> What I thought made the challenge interesting was the implicit suggestion
> that HoTT (or NCT, as Jay Sulzberger humorously suggested) was such a
> gigantic leap forwards in foundational thinking that "old-style" foundations
> could not possibly begin to compete with it.  To me, this was a really
> striking claim, especially when a concrete example was provided, that
> superficially did not look very different from any other piece of advanced
> mathematics.  I thought that something could be learned about the
> relationship between the "old" and "new" foundations by examining this
> example critically---the alleged Great Leap Forward would either be shown to
> be exaggerated rhetoric, or the rhetoric would be proved to be correct in a
> very concrete fashion.
>
> As it turns out, it seems that examining this example has been rather
> instructive (at least to me), even without rolling up one's sleeves to start
> trying to formalize Blakers-Massey in earnest.  I found Paul Levy's comments
> particularly clarifying.  It seems to me to come down to the old question
> that one can ask of any theorem, namely, what is its *real content*?
>
> For an ancient example, let's consider the Pythagorean theorem.  What is
> this theorem *really* about?  Is it a statement about the physical world? Is
> it a theorem in Euclid's system?  Or is it a theorem about the real numbers,
> in all their complete-ordered-field, continuum-hypothesis-laden glory?  Or
> is it just a *definition*?
>
> The pragmatist might find this debate pointless, because there are standard
> ways of moving between the different interpretations, so there is no need in
> practice to ask for the true Pythagorean theorem to please stand up.  This
> sort of phenomenon is commonplace in modern mathematics, where one author
> might take X to be a definition and derive Y as a theorem and another author
> might take Y to be the definition and derive X as a theorem.  Both are
> possible, but in practice, picking the right starting point can make a big
> difference.  If you pick definitions that come close to capturing the heart
> of the phenomenon of interest, then your arguments will be shorter, cleaner,
> and clearer.  A different starting point could work, but it would cost more.
>
> Without actually knowing anything about the actual content of the
> Blakers-Massey theorem, I think that something similar is going on here.
> Someone might ask, is the theorem, deep down, really a theorem about sets?
> The experts are telling us, no, the actual content of the theorem is best
> expressed purely in the language of HoTT.  If you insist on making it a
> theorem about sets, you can do so, but at a significant cost.  I suspect
> that Schreiber is exaggerating the cost, but it is obvious that there is
> some cost.
>
> This much should be relatively uncontroversial, but I think it gets more
> controversial when some proponents of HoTT suggest, or seem to suggest, that
> it is a superior foundation not just for Blakers-Massey and the like, but
> for all of mathematics.  Joe Shipman made this point.  I, like Shipman, am
> unclear whether HoTT is supposed to be a candidate for this role.  Would,
> for example, the Flyspeck project have been completed with a fraction of the
> effort if HoTT had been used?  Do HoTT proponents envision the next
> generation of undergraduate mathematics textbooks on analysis and algebra
> having their brief summaries of set theory replaced by summaries of HoTT?
> Will future generations of mathematicians no longer think of a finite group
> as a finite set equipped with a binary operation, or of the reals as a set
> of numbers?  This, to me, is the main question that I haven't seen answered
> by HoTT proponents.
>
> Tim
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom