Я вряд ли эксперт в этом вопросе (я всего лишь пользователь этих систем; я не беспокоюсь слишком много об их внутренностях), и это, вероятно, будет лишь неопределенным частичным ответом, но я знаю два основных подхода:
- Системы с независимой типизацией (например, Coq, Lean, Agda), в которых используется изоморфизм Карри – Ховарда. Утверждения - это просто типы, а доказательства - это термины, имеющие этот тип, поэтому проверка действительности доказательства - это, по сути, лишь частный случай проверки типа термином. Я не хочу говорить слишком много об этом подходе, потому что я не знаю слишком много об этом и боюсь, что я что-то не так пойму. Тео Винтерхальтер связал что-то в комментариях выше, что может дать больше контекста в этом подходе.
- Доказательства теорем в стиле LCF (например, Изабель, HOL Light, HOL 4). Здесь теорема (грубо говоря) является непрозрачным значением типа
thm в языке реализации. Только сравнительно небольшое «ядро доказательства» может создать эти thm значения, и все другие части системы взаимодействуют с этим ядром доказательства. Ядро предлагает интерфейс, состоящий из различных небольших функций, которые реализуют небольшие шаги вывода, такие как modus ponens (если у вас есть теорема A ⟹ B и теорема A, вы можете получить теорему B)или introduction-введение (если у вас есть теорема P x для фиксированной переменной x, вы можете получить теорему ∀x. P x) и т. д. Ядро также предлагает интерфейс для определения новых констант. В принципе, если вы можете верить, что эти функции точно реализуют основные этапы логического вывода базовой логики, вы можете верить, что любое значение thm, которое вы можете произвести, действительно соответствует теореме в вашей логике. Для испытателей в стиле LCF ответить на вопрос о том, что такое фактическое доказательство, немного сложнее, потому что они обычно не строят термины доказательства (например, у Изабель они есть, но по умолчанию они отключены и не используются широко). Я думаю, что можно сказать, что история того, как называются примитивы ядра, является доказательством, и если бы кто-то записал это, он мог - в принципе - воспроизводиться и проверяться в другой системе.
В обоих случаях идея заключается в том, что у вас есть ядро (средство проверки типов в первом случае и ядро вывода во втором), которому вы должны доверять, а затем у вас есть большая экосистема дополнительных процедур вокругэто, чтобы обеспечить больше удобных слоев. Однако, поскольку им приходится взаимодействовать с ядром, чтобы на самом деле создавать теоремы, вам не нужно доверять этому коду.
Все эти разные системы имеют различные компромиссы в отношении того, какие части системы находятся вядро а какие части нет. В целом, я думаю, будет справедливо сказать, что системы с зависимой типизацией имеют тенденцию иметь значительно большие ядра, чем основанные на LCF (например, HOL Light имеет особенно маленькое и простое ядро).
Есть такжедругие системы, которые, я считаю, не вписываются в эти две категории (например, Mizar, ACL2, PVS, Metamath, NuPRL), но я ничего не знаю о том, как они реализованы.