I’m currently procrastining, so here is a lecture of some interest on modern NLP:
From Deep Learning to Deep Understanding: presentation PDF by Heung-Yeung Shum (Microsoft Research):
the above via
- Math-Science Literature Lecture Series of Harvard University via
- Peter Woit’s Not Even Wrong blog
…which also has a note on Peter Scholze putting up a challenge to formalize the proof of a certain theorem using, for example, say, the Lean theorem prover:
the Lean community has already showed some interest in formalizing parts of condensed mathematics, so the theorem seems like a good goalpost.– from what I hear, it sounds like the goal is not completely out of reach. (Besides some general topos theory and homological algebra (and, for one point, a bit of stable homotopy theory(!)), the argument mostly uses undergraduate mathematics.)
If achieved, it would be a strong signal that a computer verification of current research in very abstract mathematics has become possible. I’ll certainly be excited to watch any progress
I think this may be my most important theorem to date. (It does not really have any applications so far, but I’m sure this will change.) Better be sure it’s correct…
That’s not the undergarduate mathematics I remember. Sounds challenging.