Lean Emerges as AI's Trust Layer for Verified Code

Three signals in 48 hours point to verification as AI's bottleneck: Sasha Rush's JAX-to-Lean transpiler for formally verifying ML code, a talk arguing generation is cheap while review is expensive, and Terence Tao's post on Lean's reliability. Lean's ~5,000-line kernel checks proofs independently of the AI that wrote them.

• jax-lean transpiles JAX code to Lean and proves tensor properties
• AWS demoed 32,000 lines of AI-generated Lean proofs for zlib in a week
• 96% of developers distrust AI code accuracy, but only 48% verify it
• Lean's trusted kernel is ~5,000 lines vs 500,000+ in the Rust compiler