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 , for some .

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…

### Like this:

Like Loading...

*Related*

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