But I remain very sceptical about all of these so-claimed "proofs" from AI...
The main reason is that I tried myself to use the best models that money could buy to prove some "folklore-theorems" within quantum field theory. (Only for experts: For example the linked cluster theorem for arbitrary interactions in the functional field integral formalism with a graph-theoretical formulation of the appearing reordering.)
And the pattern is always the same: The AI is creating a bulk of material that kind of goes into the "right" or "anticipated" direction, but then (and this happens almost always), somewhere along the way, it does a mistake, makes a wrong assumption, makes a simplification that doesn't hold or something similar...
The only proofs that I genuinely believe will be those that are verified with this Lean-language (this is not an advertisement; I don't even know how to code in Lean myself, but it acts as a formalizer for mathematical identities).
-- Sebastian
Last month one of my coworkers was very surprised because the AI said something was a linear function. (It was not!) He had a huge chat with the AI and the AI was very confident and even added a few examples of (other) linear functions, and continue explaining how everithing was easy because it's linear. In spite it was obvious that it was not linear and not easy, we had to reread it a few times to be sure it was nonsense and we were not missing something.
The problem is that most of the time the AI is absolutely right, so we start to doubt.
>Teams led by physicist used “BootLoops” software to produce 36 papers in weeks on everything from linguistics to health policy