The field of mathematics is smart about this and knows the difference between a pile of Lean code and understanding, and mathematicians try to get from the unintuitive explanations to something that makes more sense, e.g. https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the... (where incidentally Tao used a chatbot to help take apart the problem, but with a lot of interaction and work from his side).

Making things understandable is mathematics, and more generally a kind of intelligence, and is crucial to continued progress. You couldn't use algebraic geometry to disprove a conjecture if people hadn't organized (what could have been just) a pile of random observations into something called algebraic geometry.

Historically LLMs have done best where it's possible to train using an objectively verifiable reward function. Computer programs are pretty good on this front and so are Lean proofs. (Of course, they don't only do things you can RLVR heavily, but those have progressed fastest.) Not sure where 'making mathematical knowledge more understandable' falls on that spectrum.

Understandability isn't only important for advanced math. Keeping computer programs from becoming a mess is a challenge in high-level organization too, and the chat with the user is an explanation task. If you look online at what people say about large LLM-built codebases (SlopCodeBench is a neat effort to make make it concrete, but common wisdom seems to mostly agree on the general problem) and chatbot prose, I don't think everyone considers those solved problems!

It's hard to tell how thoroughly the labs grasp and care about this at an organization-wide level. I'm sure at least some maybe-results exist inside labs but haven't been published because the humans couldn't verify them and didn't want to be embarrassed with a false result. (Maybe also why counterexamples are a lot of the first results published: often simple to verify, even if hard to obtain.) A good sign would be if results in a few months come out more like what mathematicians consider well-written papers explaining results in a more intuitive way, fewer shocking announcements of bare counterexamples in tweets. It's probably a slow climb to get there.