Stacksのセクション3.2がスキームに対して始めるように、数学の定義を集合論に自動で解きほぐすものを想像してみてください。これは、知らないかもしれないすべての概念を再帰的に定義する方法です 誰かこれをバイブコードして、今の私たちコンピューター猿がやっていること

任意の深さの上限などがあれば、ZFCや深層の数学的論理にまで深入りする必要はありません。少しレベルを下げるだけでも助けになるかもしれません。もちろん、スキームのようなものはかなり広がっていき、N枝が再帰的に下に進むこともありますが、はい

役に立たなくても、もしかしたら見た目はいいかもしれません。

もしかしたら、MathLib Defsで一番下に落ちてみてはどうでしょうか?

正直、TLに投稿していることで自分を侵害している気がしますし、購読者だけでなく、ここ2日間ドロップダウンをクリックするのを忘れていたので、もういいやと思っています