>Teams led by physicist used “BootLoops” software to produce 36 papers in weeks on everything from linguistics to health policy

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 ALLWAYS!!!), 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