Lean Programming Language

Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code -- '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 ≤ 4

[efcl]

定理証明言語。Microsoft ResearchとかOpen AIの人がやっている

[Nyoho]

Microsoft Research製の証明機 (prover)

[darwinia]

へぇこんな言語が。

[igrep]

Microsoft Researchによる定理照明器。Z3ともまた違うんだろうかね。 => 訂正。なぜ定理証明器とSMTソルバーをごっちゃにしたんだ。。。

[ruicc]

Learn you a haskell的なものかと思ったらleanだった