6 ms·
its just as likely hallucinations will only get worse because their source data will be riddled with hallucinations
by timacles 2mo ago
its just as likely hallucinations will only get worse because their source data will be riddled with hallucinations
- eru 2mo agoYou can't hallucinate a working lean proof.
- darkwater 2mo agoBut you can hallucinate everything else.
- tempfile 2mo agoYou absolutely can. How do you know your "working lean proof" actually proves the theorem you intended it to?
- lanstin 2mo agoOne 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.
- eru 2mo agoYou read the stated theorem?