Comment by pas
5 hours ago
... what is understanding of mathematics anyway? if some AI result helps a mathematician to solve more problems I would say then that it gave them some understanding, but just as there are proofs that span hundreds of pages it's likely that soon proofs will be long Lean programs and studying them will be part of mathematics, just as studying Go played by AI.
(see the open (Lean) label for Erdos problems https://mathstodon.xyz/@tao/116987866420438091)
https://davidbessis.substack.com/p/the-fall-of-the-theorem-e...
This blog post talks in depth about what you're talking about. It may interest you. It even talks about the future where math proofs are just Lean programs, and why that won't necessarily be a good thing.
It's worth a read, even if it's long AF.