@tao these are great videos! Any chance you would be willing to just do a very basic starter video for those of us still learning Lean (probably many of us)? It doesn't have to be totally from scratch, but would be very interesting to just go through proving some very simple theorems. Could try the quadratic formula, the Pythagorean theorem*, whatever. Would also be interesting to see how well the LLM/AI can do these things on its own and where it tends to need human feedback.

(*This seems a bit nontrivial to do in Lean, as how do you even set up the problem without presupposing an L2 norm to begin with?)