That's why this proof and all the other high profile AI proofs were written in lean, which allows you to verify them in a formal deterministic language. You sti

That's why this proof and all the other high profile AI proofs were written in lean, which allows you to verify them in a formal deterministic language. You still might not understand it as a human, but any computer with a simple processor can verify the proof's correctness. And from there you will undoubtedly see other people make sense of the proof's key steps using AI too. And the models might even pick up on further details useable for other proofs that humans didn't see. In the end I'm 100% convinced that abstract math will eventually be primarily done by computers, similar to how linear algebra and numerics have been done exclusively done by computers for a while. Noone would even consider multiplying a 100x100 matrix by hand anymore, if only because it is much more likely that you as a human will make a mistake.