想像一個東西，可以自動解釋數學定義，直到集合論，就像 Stacks 第 3.2 節開始為一個方案做的那樣，作為遞歸定義你可能不知道的每個概念的方式。 有人把這個編碼出來，或者不管我們這些電腦猿人現在做什麼。

有一些任意的深度上限或其他東西，無需深入到 ZFC 或某些深奧的數學邏輯。只需幾層的下降就能有所幫助。顯然，有些東西（比如計劃）會像瘋了一樣展開，所以你會有 N 個分支遞歸地向下，但就是這樣。

如果不實用，也許可以很漂亮？

也許可以去 mathlib 定義找尋最低點？

老實說，發佈在時間線上而不只是給訂閱者，讓我感覺像是在侵犯自己，但這兩天我一直忘記點擊下拉選單，所以隨便吧。