Interesting post. The First Proof experiment really showed us the near future of AI/math interactions, some impressive success, but also lots of extremely hard to verify text, misformulated lean "proofs" etc. but progress on AI does math has indeed been impressive
I highly recommend this short book(story).
One of the best I have seen in my life :)