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 (note: the blueprint link no longer works).
No comments:
Post a Comment