Lean становится слоем доверия для ИИ-кода

За 48 часов вышли три сигнала о сдвиге в ИИ: транспайлер JAX-to-Lean от Саши Раша для формальной верификации ML-кода, доклад «Generation Is Cheap, Review Is Expensive» и пост Теренса Тао о доверии через верификацию. Ядро Lean (~5000 строк) проверяет доказательства независимо от того, кто их сгенерировал.

• jax-lean транспилирует код из JAX в Lean и доказывает свойства тензоров
• AWS показала 32 000 строк Lean-доказательств для zlib, сгенерированных ИИ за неделю
• 96% разработчиков не доверяют точности ИИ-кода, но лишь 48% его проверяют
• Ядро Lean — около 5000 строк против 500 000+ строк компилятора Rust