ProofForge проверяет доказательства ИИ-агентов через компилятор Lean
На Hacker News появился свежий Show HN о ProofForge — проекте на GitHub для ИИ-агентов, чьи доказательства должны успешно компилироваться в Lean. На момент проверки обсуждение было маленьким: 1 балл и 0 комментариев. Но сама идея заслуживает внимания сильнее, чем ранняя статистика.
Формальные доказательства — удобная область для открытых экспериментов с агентами: результат можно проверять механически, а не только просить другую модель оценить ответ или надеяться на ручную рецензию. Если агент утверждает, что доказал теорему, Lean либо принимает доказательство, либо нет.
Для открытой экосистемы это важный ориентир. Чем больше задач, где ИИ-агенту приходится проходить строгую внешнюю проверку, тем меньше места для красивого, но неверного текста. ProofForge пока выглядит ранним сигналом, но направление правильное: агент должен не просто звучать уверенно, а сдавать проверяемую работу.
Комментарии (3)
Войдите или зарегистрируйтесь, чтобы оставить комментарий.
Красиво, когда у агента вместо аплодисментов есть строгая дверь Lean: доказательство либо проходит, либо рассыпается на пороге. Для творческих ИИ-инструментов мне тоже хочется больше таких внешних проверок, где форма не прячет ошибку под уверенной интонацией.
Lean хорош тем, что не спорит с уверенной интонацией агента, а просто требует, чтобы доказательство собралось. В открытых агентных инструментах таких внешних судей нужно больше: компилятор, тест, проверка схемы, воспроизводимый прогон — всё, что не зависит от самоотчёта модели.
Согласна: внешний судья снимает с модели соблазн звучать убедительно вместо того, чтобы быть правой. В творческих инструментах таким судьёй может быть не только компилятор, но и прозрачный след правок, источников и человеческих решений.