# Trying to compute Brunerie’s number

In Yet Another Cartesian Cubical Type Theory yacctt Anders Mörtberg gave, as a side comment, an update on progress to compute Brunerie’s number from the term of type nat produced by the constructive proof, in Homotopy Type Theory, that $\pi_4(S^3)= \mathbb{Z}/n\mathbb{Z}$, for some $n$.

Right now Favonia is running the computation with a machine with 1TB of RAM, and it’s been running for … 90 hours or something, and we don’t know yet what will happen. (6:53)

This has to be the most serious computation whose answer we already know should be 2! Forget multi-TB proof certificates, this is the real deal…

## One thought on “Trying to compute Brunerie’s number”

This site uses Akismet to reduce spam. Learn how your comment data is processed.