Comment by 8note
4 hours ago
i think id almost worry more that ai can solve problems in latent space that it cant translate back to tokens because decoding ruins it, and that we wont be able to come up with concepts that we can map to properly decode those solutions in a way people understand
... 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.