Lean Programming Language

Lean is an open-source programming language and proof assistant 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 → 1

[efcl]

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

[Nyoho]

Microsoft Research製の証明機 (prover)

[darwinia]

へぇこんな言語が。

[igrep]

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

[ruicc]

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