[FOM] Foundational Challenge

[Joe Shipman]

I’m not disputing that that particular result has a shorter formal proof in HTT. I did say, or intended to say, that the amount by which I was asking for improvement in the *proof* was greater than the amount of work already needed simply to *state* the proposition in ZFC. If one regards all the work required to *define* Homotopy Groups of Spheres, then obviously HTT will do better than ZFC, but I already knew that. 

People working in ZFC have already done the work they need to state the propositions they are interested in. The function f(n,k) calculating the kth homotopy groups of the n-sphere (represented using some standard easy coding of finitely generated abelian groups) may be considered from 2 starting points: a development in ZFC that has defined it, and a development in HTT that has defined it.  From these starting points, does HTT provide any improvement in the amount of work needed to actually calculate it? (That is, the incremental  proof length needed to derive propositions of the form f(n,k)=G for specific values of n,k,G.)

— JS

Sent from my iPhone

> On Jan 13, 2020, at 12:08 PM, Timothy Y. Chow <tchow at math.princeton.edu> wrote:
> 
> On Sun, 12 Jan 2020, Joe Shipman wrote:
>> This is an elementary result that is easy in ZFC, I’m interested in if they have calculated anything new from HTT. My understanding is that Sergeraert and Rubio’s work in the 90’s on effective homotopy calculations is still the main algorithm used, but it would be nice to know if HTT has resulted in either better results about their algorithms, or better algorithms.
> 
> I confess to a feeling that the goalposts have shifted.
> 
> Your original challenge was for an arithmetical result with a significantly shorter formal derivation from first principles.  You also specifically said that "reaching old results more easily" would count.
> 
> Now you dismiss pi_n(S^n) = Z as "easy in ZFC."  But we're talking about *formal proofs*.  How easy or short is it really in ZFC?  Is there a formal proof in Mizar whose length we can measure?  Have you formalized the proof yourself both ways and confirmed that the proof is shorter one way or the other?  (Here I'm setting aside Peter LeFanu Lumsdaine's valid points about what the theorem in question really is.)  I suspect not.
> 
> I don't see the point of issuing challenges if you're not prepared to adjudicate submissions fairly.
> 
> Tim_______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom