представьте себе штуку, которая автоматически разворачивает математические определения до теории множеств, как это начинает делать Раздел 3.2 Stacks для схемы, как способ рекурсивно определить каждую концепцию, которую вы, возможно, не знаете кто-нибудь напишите код для этого или что-то в этом роде, что мы, компьютерные обезьяны, делаем в эти дни

с некоторым произвольным пределом глубины или что-то в этом роде, нет необходимости углубляться в ZFC или какую-то глубокую математическую логику. Просто несколько уровней вниз могли бы помочь. Очевидно, что некоторые вещи (например, схемы) разветвляются как сумасшедшие, так что у вас будет N ветвей, рекурсивно уходящих вниз, но да.

если не полезно, может быть, красиво?

может, стоит обратиться к определениям mathlib для самого низкого уровня?

честно говоря, мне кажется, что я нарушаю свои собственные границы, публикуя это в TL, а не только для подписчиков, но я забыл нажать на выпадающее меню эти последние 2 дня, так что к черту это.