notes

Lean maybe not needed for math (a la deepmind papers) but still wonderful that you can let the models go out and just learn (like chess, like go)

Maybe mathematicians will become like art curators - artists exist, and they can even explain their own work (3b1b thinks that the models will be good enough at expositing their own work, in the same way that shannon's and einstein’s and feynman’s groundbreaking papers are all relatively lucid)