Palomar: реестр проверенных доказательств на языке Lean

Доказательства, сгенерированные моделями, пошли валом, и часть их оформлена на Lean — языке, где машина проверяет каждый шаг. Проблема не в проверке, а в доверии к чужому репозиторию: непонятно, проходят ли заявленные утверждения проверку типов, нет ли в них обхода вроде допущенной аксиомы и совпадает ли формальная запись с тем, что утверждают словами.

Palomar — реестр, где доказательства прогоняются и помечаются как проверенные по этим трём пунктам. Смысл в том, что неэксперт получает ответ на вопрос «это доказано или так написано» без чтения самого репозитория.