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

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

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