Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code
/-- A prime is a number larger than 1 with no trivial divisors -/
def IsPrime (n : Nat) := 1 < n ∧ ∀ k, 1 < k → k < n → ¬ k ∣ n
-- 'Grind' efficiently manages complex pattern matching and
-- case analysis beyond standard tactics.
example (x : Nat) : 0 < match x with
| 0 => 1
| n+1 => x + n := by
grind
-- Automatically solves systems of linear inequalities.
example (x y : Int) :
27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45
→ -10 ≤ 7*x - 9*y → 7*x - 9*y > 4 := by
grind
Does anyone have experience with Lean? Can it be useful for implementing algorithms or logic beyond mathematical proofs, for software libs?
Yeah you can use it for normal software. It is very complex though, and the documentation assumes you already have a PhD in formal verification.
I haven’t tried Lean, but one of my university courses had us use Dafny, which essentially states the pre- and postcondition of a function. If it can’t prove the conditions are fulfilled, you get an error. This essentially turns all of your bugs (that is, unexpected behaviour) into specification problems. It can also prove that loops eventually end, and the data in a structure follows a specific pattern.
The comment in the first example is wrong, it should be no nontrivial divisors.
Quite ironic, that they can prove theorems about their code, but the comments can’t be checkt by the compiler, resulting in their first math example being wrongly described.Lean is a functional programming language, and can be used as one i.e. you can make absolutely anything in it. But it’s mostly meant for theorem proving, so you won’t get any libraries/support for regular software dev. That said, I do know folks who have written complex software (I remember seeing the code for a raytracer) in it, so it’s definitely doable.
Lean is a quite advanced design.
