Keep in mind that I'm using "information" in the information-theoretic sense. One could argue that because that particular solution to NS is provable, it is therefore implied by the propositions they started with and adds no new information.

And I'd still rather read a human's interpretation of the solution to NS than read whatever the LLM wrote.