The output would be a string containing the proof, which a deterministic, non-LLM proof-checker could decide whether it’s correct or not.
This part seems like an optimistic statement. Do we have LLMs outputting proofs in a consistently correct format that prof checkers can accept?
From the article:
That’s some hard-hitting journalism right there