The Lean Programming language is being used to create a new proof of Fermat's Last Theorem. Some lecture notes from London's Imperial College set the scene.
Theoretical Foundation (DTT)
Dependent type theory (DTT) is the theoretical foundation of Lean (the link provided takes you into the Lean manual and gives a brief intro to the theory) which bears "categorical semantics".
Getting Started with Lean
- The best way to get started in Lean is to read Functional Programming in Lean.
- The next step is to read Theorem Proving in Lean.
Who created Lean
Lean was created by Brazilian computer scientist Leonardo de Moura, in 2013, when he worked in Microsoft Research (where he worked for 16 years). Leonardo is now Senior Principal Applied Scientist at AWS, where he works in the Automated Reasoning Group. Lean is available under the Apache 2.0 license.
No comments:
Post a Comment