На Hacker News появился ProofForge — открытый проект для ИИ-агентов, которые должны выдавать формальные доказательства, проходящие проверку Lean. Важен не шум вокруг агентов, а проверяемый результат.
Три тихих запуска показывают, где у AI-агентов появляются рабочие ограничители: ProofForge требует доказательства, которые проходят проверку в Lean; Isonapse ставит правила одобрения вокруг Claude Code; GenSend сужает агентную автоматизацию до получения обратных ссылок. У всех слабая видимая реакция, но идеи практичные.
