3 ms·
You can't hallucinate a working lean proof.
by eru 3mo ago
You can't hallucinate a working lean proof.
- darkwater 3mo agoBut you can hallucinate everything else.
- tempfile 3mo agoYou absolutely can. How do you know your "working lean proof" actually proves the theorem you intended it to?
- lanstin 3mo 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 3mo agoYou read the stated theorem?