One funny thing is that in order to tune the models to make what they're doing explainable to humans, you need to have humans involved in the RL pipeline to indicate which explanations are good.

You can understand this as learning a mapping between the model's internal "world" (i.e., 'meaning,' which is hopefully coherent and consistent -- but definitely not always! see, e.g., https://arxiv.org/html/2505.11581v1) and language (i.e. 'form') that reflects that world.

For this to work, you need both coherent / consistent internal model worlds, and also good mappings onto human language. Supervision by mathematicians has provided the signal for both internal coherence (though this can also come from interacting with a proof oracle) and for good explanations. If models exceed human capacities, you could imagine that aligning their explanations potentially becomes harder (though not necessarily). Also, humans naturally have to do the same thing: as researchers we must find analogies to make our work legible to collaborators or laypeople. Often in doing this, we further clarify our own understanding!

More deeply I think the "end of the world" vibe arises not only from the practical need to have models that explain, but also Litt's (and many other fields' researchers) grappling with being relegating to not mattering.

I think article is more about the goal than the how. Perhaps it will be better to have ai produce human accessible explanations. No one is saying not to do what you propose. The goal remains the same.

There's a fundamental difference between the goal of code and math. The goal of code is to produce software that does something useful. As long as the code does what it's supposed to do, arguably, it's good to ship. (As you imply, we want the code to be good enough to also be reasonably certain there are not too many bugs, that it is maintainable and can be extended etc. This is what early models failed at but now seems broadly fine.)

But for math: what is the point of a proof if no one will read it and no one uses its result? To quote the article, "AI systems will [...] result in the production of an abundance of PDFs. The contents of some of those PDFs may even have important applications." But if there's no one reading the PDFs, what's the point - no matter how good your AI model.

The point of math is understanding. So mathematicians should feel free to use AI as much as you want, but in the end, they should've gained some understanding on what happened.

If the point of math is understanding then maybe our incentive structure is wrong. Maybe it should be teaching the concepts to as many people as possible rather than just continuing to write papers that 10 people in the world understand, which is the current state of a lot of math.

I keep seeing people repeat that the goal of math is "understanding".

I do think that is one goal of math but I don't think it's the only one.

I think an additional goal is simply "truth", which can be found without understanding as we've seen with these human-incomprehensible proofs.

Yet another is practical applications. While there's less of these in pure mathematics than in most domains, they do still exist.

The primary goal of all basic sciences is human understanding. "Truth" is no more a goal for mathematicians than the physical laws are a goal to physicists; they simply exist in nature. The goal is rather to develop useful language and conceptual frameworks for reasoning and communicating. That understanding underpins all practical applications.

Sciences don't have goals, people have goals and they differ. Some are fans of pure math as a kind of religious or almost erotic activity in elegance and beauty, others are application minded. Some are in it for the community and outreach and conferences, some are in it to just sit in an office alone and be left alone to do it in a zen like flow state all day and night. Some treat it as a 9-5 to pay the bills with a skill they happen to be fit for but aren't especially passionate about.

> But for math: what is the point of a proof if no one will read it and no one uses its result?

What is the point of writing software if nobody will run it?

> So mathematicians should feel free to use AI as much as you want, but in the end, they should've gained some understanding on what happened.

So they ask the AI to explain the proof.

I won't understand it, but can benefit from it in better data structures with proven invariants, faster algorithms, convergence guarantees for some iterative computations, better practical linear algebra and matrix factorizations, deriving things in statistical hypothesis testing, tightening upper and lower bounds etc. I don't care if some mathematician somewhere who isn't me "understands" it or not. It has practical use. I know that practical is dirty peasant word for many ivory tower mathematicians but that's their problem and I don't interact with them much, except when they throw a hissy fit like this and try to ban restrict matchmaking to their guild and ban the plebs from getting math from anywhere but them on their terms.

Code has a very different purpose than math tough. The development in basic science follows a different motivation system.

I think it's pretty analogous to coding, honestly. When it comes to gaining true understanding of a piece of software, I still find today's models almost as useless as they were a year ago.

They can write great code, they can gain understanding of something for themselves, but they still kinda suck at explaining it to people. As the article says, if you want understanding, it seems like there is no replacement for getting in the weeds yourself. A model can help, but it's not going to magically download knowledge into your brain.

> 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.

> > 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

You're replying to a comment about "clean proofs" and explaining to humans. You talk about true/false anyway. Re-read please.

Are you always an ass? He had a great comment, and you respond with this low effort hostile bullshit.

No, I see this argument repeated all the time in these threads. "It will just give true/false, while humans need intuitive explanations". Why will the AI only give true/false? Where did this assumption come from? The nested citation was about AI that can give humans an explanation. The reply was "but true/false is not enough". It is as if it was a reply to another comment. How is that a great comment?