I didn't mention it in the video, but I've already used ChatGPT to ask questions about Lean, and it worked. I had to specify that it was Lean 4 because a significant portion of the material available online is about Lean 3, which is quite different.Links:https://github.com/adolfonthttps://github.com/adolfont/learning-leanhttps://lean-lang.org/https://lean-lang.org/functional_programming_in_lean/title.htmlType Theory for All with Leo de Mourahttps://www.typetheoryforall.com/episodes/z3-and-lean-the-spiritual-journey