Comment by logicprog

> A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.

Yeah, because before now there's been literally zero proof of an automated theorem prover scaffold around the LLMs being used, and big counterexamples and such being found, with raw chat logs available, where no such thing was used.

> Now they have it in writing.

Yeah, because now it's actually being done. They talk about it as a novel thing, because it is. You don't get to claim being "right all along" from this