#Lean
4 related articles
Lean Officially Integrates Verified Kernel, Achieving Breakthroughs in Both Reliability and Performance
Lean theorem prover officially releases a formally verified kernel, improving proof trustworthiness and strengthening the trusted computing base. This article analyzes its ecosystem impact, performance trade-offs, and community reaction.
Getting Started with Lean Programming: Turning Requirements into Machine-Verified Theorems
From bounded counters to inventory state invariants, this article shows how to use Lean to turn requirements into mathematical specifications and machine-checked proofs, and explains what formal verification does and does not guarantee.
OpenAI Releases Formal Math Proofs: 4 Open-Source AI Math Tools You Can Run Locally
OpenAI open-sources Lean formal proofs for Navier-Stokes problems. This article covers 4 open-source AI math tools—positioning, capabilities, and hardware requirements—to help you choose the right one.
TutorialsTerence Tao Uses Claude Code for Math Proof Review: Red Team Tasks More Valuable Than Blue Team
Terence Tao demos how Claude Code assists Lean math formalization through red team tasks: code review, style checking, and refactoring rather than proof generation.