уявіть собі пристрій, який автоматично розплутує математичні визначення до теорії множин, як це починає робити Stacks Section 3.2 для Scheme, щоб рекурсивно визначити всі поняття, які ви можете не знати Хтось вібкодує це чи що там зараз робимо комп'ютерні мавпи

З якоюсь довільною глибиною чи чимось таким, немає потреби занурюватися в ZFC чи якусь глибоку математичну логіку. Кілька рівнів нижче можуть допомогти. Звісно, деякі речі (наприклад, схеми) розкидаються як шалені, тож N гілок рекурсивно знижується, але так

Якщо не корисний, то, можливо, гарний?

Можливо, варто перейти до Mathlib Defs для дна?

Чесно кажучи, мені здається, що я порушую себе, публікуючи на TL, і не лише для підписників, а останні 2 дні я забував натиснути на випадаюче меню, тож хай буде