Comment by timacles
2 months ago
its just as likely hallucinations will only get worse because their source data will be riddled with hallucinations
2 months ago
its just as likely hallucinations will only get worse because their source data will be riddled with hallucinations
You can't hallucinate a working lean proof.
But you can hallucinate everything else.
You absolutely can. How do you know your "working lean proof" actually proves the theorem you intended it to?
One of the concerns of the new LLM made lean proofs is ensuring they are using standard MathLib formulations in the theorem, so (quoting something in I longer recall the source of) a Grothendieck scheme is indeed what the reader and world know as a Grothendieck scheme.
You read the stated theorem?