想象一个东西，可以自动将数学定义解开到集合论，就像 Stacks 第 3.2 节开始为一个方案做的那样，作为递归定义你可能不知道的每个概念的方式。 有人把这个编程实现一下，或者不管我们这些计算机猿猴现在在做什么。

有一些任意的深度上限之类的，不需要深入到 ZFC 或者一些深奥的数学逻辑。只需下降几层就可以了。显然，有些东西（比如方案）会疯狂地扩展，所以你会有 N 个分支递归地向下，但就是这样。

如果没有用，也许很漂亮？

也许可以去 mathlib 定义找最低点？

老实说，发在时间线上的感觉就像是在侵犯我自己，不仅仅是为了订阅者，但这两天我一直忘记点击下拉菜单，所以算了。