Claude can sometimes prove it

Claude Code от Anthropic демонстрирует неожиданно высокую способность к интерактивному доказательству теорем (ITP) — области, где даже эксперты сталкиваются с трудоёмкими и сложными процессами. Этот ИИ-агент успешно справляется со многими сложными шагами доказательств самостоятельно, хотя пока требует руководства человека для полной формализации.

Такой прогресс открывает перспективы широкого использования инструментов вроде Lean без необходимости глубоких экспертных знаний, что может ускорить верификацию критических систем, криптографии и компиляторов. Практический совет: попробуйте сами инструменты вроде Claude Code или Gemini CLI на знакомых задачах — это обойдётся примерно в $20–100 в месяц.

Комментарии (60)

Участники обсуждают потенциал LLM (особенно Claude Code) в генерации формальных доказательств и кода с использованием инструментов вроде Lean, отмечая, что ИИ часто успешно справляется с первой частью задачи, но испытывает трудности с завершающими, самыми сложными этапами.
Подчеркивается фундаментальная проблема: сложность не в написании кода, а в создании точных и корректных спецификаций и требований, что является ключевым для формальной верификации и доказательства правильности программ.
Высказывается мнение, что сочетание генеративных ML-моделей с формальными методами — многообещающий путь вперед, так как LLM снижают усилия на реализацию, а формальные методы — на проверку, компенсируя слабые стороны друг друга.
Обсуждаются практические сложности: необходимость жесткого контроля за выводом ИИ, риск получения ложных доказательств, которые лишь выглядят корректно, и важность эмпирической валидации результатов, сгенерированных ИИ.
Отмечается, что архитектурные решения и изменяющиеся требования часто делают формальные доказательства непрактичными для большинства реальных проектов, где код не статичен, а правильное абстрагирование и разделение ответственности важнее тотальной корректности.