They are new proofs and for sure useful but as far as I’ve understood mainly interpolative. E.g. an LLM can “create” a poem about a purple chicken as it has datapoints for “purple” and “chicken”, so it can create something plausible inbetween.
Similarly, in my mind it can interpolate proofs by interpolating between data points for technique A and technique B. This is novel and brute-forcing proofs this way is useful. It is analogus to how sometimes it can generate programs that pass unit tests, I think.
However, creating fundamentally new concepts outside of the interpolated datapoints is not something I am convinced of. Maybe it can extrapolate some things, if correct add it as a data point, continue. Essentially a search, and it would be amazing if this works and maybe we can get some recursive improvement this way. But the “ideas” it will use to conduct this search are a function of the input data points as well, and thus in my view fundamentally limited in novelty. I am not discounting the usefulness, but I am not convinced you can just keep doing this indefinitely scaling intelligence exponentially.
Of course nobody can know yet really and I am just speculating just like you. But I also think the “experts” Sam and Dario also don’t know, and given their incentives I am not really convinced by them.