# More ICM2018 videos online

The Laudatio videos for the Fields and Chern medals, the Nevanlinna, Gauss and Leelavati prizes, the Emmy Noether and Abel lectures as well as the medal and prize winners’ lectures are now on YouTube! Handy links:

One thing I learned from the Laudatio for Peter Scholze is that Serre’s Deligne’s weight monodromy conjecture is, approximately, the p-adic analogue of the Riemann hypothesis part of the Weil conjectures (which Serre Deligne had proved for function fields over finite fields). I somehow missed this whenever I’d read statements that Scholze had proved (cases of) this conjecture. You can read Saito’s technical article on Scholze’s work on this here.

Update 20 September: And all the plenary talks are up! See this playlist.

# 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…