Comment by tempfile

2 months ago

You absolutely can. How do you know your "working lean proof" actually proves the theorem you intended it to?

2 comments

tempfile

Reply
lanstin  2 months ago

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.