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