> Similarly now we're getting AI doing math. The proofs compile but are a mess. So just make the models better at writing clean proofs and explaining what they'

> Similarly now we're getting AI doing math. The proofs compile but are a mess. So just make the models better at writing clean proofs and explaining what they're doing to humans. That's the end of it. The assumption here is that the true/false of the theorem is the important outcome. While it is certainly part of it, a big part of maths is the understanding you gain from a proof. Many of the best proofs elegantly explain some aspect of the maths which was previously unclear and expand our understanding of the world. To use a programming related example, imagine that an LLM spits out a solution to the travelling salesman problem which works in O(n) time. On the one hand that's very convenient for whatever problem you happen to be trying to solve at the time...but there's also an answer to P=NP in there! The former means your delivery drivers app works a bit faster on their busy days, the latter fundamentally shifts how humanity thinks about certain problems. Going back to the maths, there have been theorems that were proved (by people) where the proof is broadly seen as 'unsatisfactory' in that it doesn't really expand our understanding. I assume some of these LLM proofs are a bit like that: we now know that the thing is true, but we really want to know why it's true, and how that changes our understanding.