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?
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.