[FOM] Foundational Challenge

[Timothy Y. Chow]

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