Tuesday, 30 December 2025

Leaning in on Lean

Lean is an open-source programming language and proof assistant. AWS uses Lean and "verification-guided development" to verify Cedar, the AWS authorization policy language.

Lean is being used to attempt a computer proof of Fermat's Last Theorem using the blueprint.

No comments: