はてなブックマーク

Lean について Lean は容易に正しく保守性の高いコードを書くことができるよう設計された，純粋関数型言語です．依存型という表現力の高い型システムを備えており，アルゴリズムなどが本当に意図したものを返すことを証明することができます． Lean は証明支援系でもあり，数学の証明を検証する能力を備えています．Lean で証明を書いている限り，コンパイルが通れば証明は正しいと自信を持つことができます． そして Lean はパワフルです．いま示すべきことと得られていることを逐一表示できるのはもちろん，証明の一部を自動化したり，強すぎる仮定を自動的に検出したりすることもできます． import Mathlib.Tactic /-- フィボナッチ数列の線形時間の実装 -/ def fib (n : Nat) : Nat := (loop n).1 where -- ヘルパー関数を定義する loop

Mathematics in type thoery 日本語訳 原文は Kevin Buzzard 氏によるブログ記事 Mathematics in type theory. です． この翻訳について この翻訳は有志による非公式翻訳です．翻訳に際して，表現を大きく変えた箇所があります． また, 用語の訳が一般的でない可能性があります．誤りを含む可能性もあります．ご了承ください． また，原文のブログ記事が 2020 年のものであるため，一部記載している事項が現在とは異なる可能性があります． 誤字脱字，内容の誤りの指摘，翻訳の改善の提案を歓迎いたします． この日本語版のGitHubリポジトリまでお寄せください． 翻訳に際して，機械翻訳サービスDeepL翻訳を参考にしました．