Lean (証明アシスタント)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/05/13 14:48 UTC 版)
Lean は純粋関数型プログラミング言語のひとつである。また、同時に証明支援系(theorem prover)でもある。帰納型を伴うCalculus of constructionsと呼ばれる型システムに基づいている。純粋関数型言語であるが、functional but in-place と呼ばれるプログラミングパラダイムに基づいており、効率性を重視している。
- ^ “Lean Prover About Page”. 2023年7月7日閲覧。
- ^ a b c Sebastian Ulrich (2023). “An Extensible Theorem Proving Frontend”. Karlsruhe Institute of Technology. "1.3.4 A Short History of Lean"
- ^ “Releases/v3.0.0”. GitHub. 2024年4月27日閲覧。
- ^ “Release v4.0.0-m1 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
- ^ a b c Leonardo de Moura, Sebastian Ullrich (2021). “The Lean 4 Theorem Prover and Programming Language”. 28th International Conference on Automated Deduction (CADE-28).
- ^ “The Lean Mathematical Library”. mathlib community. 2024年3月25日閲覧。
- ^ “Mathlib porting status”. 2024年3月25日閲覧。
- ^ “Mission - Lean FRO”. Lean FRO. 2024年3月28日閲覧。
- ^ “Release v4.0.0 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
- ^ “What is the Xena project?”. Kevin Buzzard. 2024年4月27日閲覧。
- ^ “Completion of the Liquid Tensor Experiment”. leanprover community. 2024年4月10日閲覧。
- ^ “@tao@mathstodon.xyz”. mathstodon.xyz. 2024年4月10日閲覧。
[続きの解説]
「Lean (証明アシスタント)」の続きの解説一覧
- 1 Lean (証明アシスタント)とは
- 2 Lean (証明アシスタント)の概要
- 3 Lean の言語仕様と機能の概要
- 4 関連項目
- 5 外部リンク
- Lean_(証明アシスタント)のページへのリンク
