коллекцию максимально подробных формализаций в языке логики предикатов тех или иных теорем? Помню, сюда скидывали такую формализацию теоремы Геделя
Есть где-то, но я не помню, где
Нашёл: https://www.isa-afp.org/
Теорем вне логики или речь идёт о формальных доказательствах метатеорем в логике?
Именно в логике предикатов? Обычно люди используют что-нибудь более выразительное.
Да, например HOL.
И ещё https://behemoth.cl.cam.ac.uk/search/ в придачу чтобы искать по AFP и окрестностям.
То, ссылку на что ты скинул — Archive of Formal Proofs.
Обсуждают сегодня