[FOM] Foundational Challenge

[Timothy Y. Chow]

Joe Shipman wrote:
> I claim that alternative foundations for mathematics ought to meet a 
> similar test---help working mathematicians find new results or reach old 
> ones more easily.
>
> Examples, please.

In case you missed it in my other FOM post, here's a paper that explains 
how the authors have formalized pi_n(S^n) = Z in homotopy type theory.

https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf

Maybe you'll be able to understand the technicalities better than I can. 
There are of course a couple of obvious caveats:

1. Swept under the rug is the translation of their theorem, which is 
expressed in type theory, into arithmetic.  This should be compared to the 
work needed to translate "pi_n(S^n) = Z" from set theory into arithmetic.

2. They are not explicitly trying to meet your challenge, and so their 
argument may not be "optimized" for that.

Nevertheless it seems to be a good test case for your challenge.

Tim