9 ms·
You absolutely can. How do you know your "working lean proof" actually proves the theorem you intended it to?
by tempfile 3mo ago
You 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?