Lean (証明アシスタント)
LeanプロジェクトはGitHubでホストされているオープンソース(英語版)・プロジェクトである。2013年にMicrosoft ResearchのLeonardo de Mouraによって立ち上げられた。
Leanには(Visual Studio Code拡張機能および言語サーバプロトコル(英語版)サーバーとして実装された)インターフェイスがあり、他の対話型定理証明系と区別される。Unicode記号をネイティブでサポートし、「×」に対する「\times」ようなLaTeXに似たシーケンスを使用して入力できる。またLeanはJavaScriptにコンパイルしてWebブラウザからアクセスでき、メタプログラミングを広範囲にサポートする。
2017年からスタートし、ユーザーが管理するライブラリmathlib には、最大規模のLeanで正規化された数学コレクションを含む。2023年2月現在、mathlibは100,000以上の定理と1,000,000行のコードを含む。
Leanの以前のリリースでは、システムロジックのいくつかのコア部分は改造されることに従順ではなかった。
システムのこれらの部分を改造したいユーザーはLeanのC++実装を(直接)変更する必要があった。さらに、仮想機械の解釈に伴うオーバーヘッドは、Leanの効率がCoqなどの他の証明アシスタントと競合できないことを意味した。2021年に、Leonardo de MouraとSebastian UllrichはLean 4をリリースした: 前述の2つの批判に対処することを目的として、Lean定理証明系それ自体を自分自身の中で再実装したものである。Lean 4はコンパイルされるCのコードを生成して、効率的なドメイン固有の自動化の開発が可能になった。Lean 4はLean 3との後方互換性はない。
Leanは数学者のトーマス・ヘイルズ(英語版)とケビン・バザード(英語版)の注目を集めた。ヘイルズはこれを彼のプロジェクト「Formal Abstracts」に使用している。バザードはXenaプロジェクトにそれを使用している。Xenaプロジェクトの目標の1つは、インペリアル・カレッジ・ロンドンの学部生の数学カリキュラムにあるすべての定理と証明をLeanで書き直すことである。