|
|
|
|
|
|
by lanstin
6 days 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. |
|
|