Reminded me of this quote: the problem with machine learning is that it's the machine that does the learning

> but I would like to understand the problem, too

But why should it be the case that this is always possible?

It's entirely reasonable that the set of useful mathematical proofs is a proper superset of human intelligible useful proofs.

In fact, to argue the contrary would imply there is something incredibly remarkable about human cognition.

Mathematics has always been an experimental science to some extent. While Newton, Euler and Gauss would spend a lot time calculating numerical approximations by hand, modern mathematicians have been doing the same using computers and software. And once an a clear picture emerge about what’s going, you can start to formalize that and attempt to prove and communicate your results in the standard definition, proposition, lemma, theorem scheme. (Btw there is even a journal called Experimental Mathematics devoted to this approach).

I don’t see that LLMs will fundamentally change this, but rather accelerate the speed of mathematical research.

Some computer generated proofs might of course be hard to understand, but at least their existence gives another data point work with.

Doing Mathematics is more than proving something, that’s just the end of a long road spent pondering at one’s desk about how things could work out.

To bluntly put it in a nutshell, and state the obvious:

If you don’t understand the problem you can’t be sure that the computer does.

Reminds me of a quote from Tsoding

> “Programming is understanding. If you don't understand what you are doing, you are not programming. You are generating text.”

Perhaps a proof without understanding is just generating numbers.