⊢
プログラミングの探求に、数学は欠かせません。その数学をプログラムとして扱える言語、Lean 4 のセットアップから始めていきます。
Lean 4 を始めてみます。プログラミングを深く探求していくと、どこかで必ず数学的な考え方にぶつかります。そんな数学を、証明という形でプログラムとして直接扱えるのが Lean です。
Definition — Lean とは
Lean は関数型プログラミング言語であり、同時に定理証明支援ツールでもあります。型を使ってプログラムを書くのと同じやり方で、数学的な命題を記述し、その証明をコードとして組み立てていくことができます。
この記事では、Lean 4 の環境構築から手を動かし始め、以降の記事でも学習過程を少しずつ載せていく予定です。
インストール
公式のインストール手順は以下のページにまとまっています。
macOS であれば、まず Homebrew を入れ、続けて Lean のバージョン管理ツールである elan をインストールします。
bash
/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)" curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
elan はプロジェクトごとに必要な Lean のバージョンを切り替えてくれます。
エディタ環境を整える
Note
自分は JetBrains 製の IDE に慣れているので、今回は以下のプラグインをインストールして使うことにしました。もともと Lean の開発者はMicrosoft Researchのレオナルド・デ・モウラだからか、VSCodeが主流のようなので、特に理由がなければVSCodeの方が良いようです。
プロジェクトを作成する
Lean のビルドツール lake を使って、新しいプロジェクトを作成します。
bash
lake new LearnLean lib.lean
実行すると、以下のファイルが生成されます。
lakefile.lean
プロジェクトの設定ファイルです。依存関係やビルドオプションを定義します。
lean-toolchain
このプロジェクトが使用する Lean のバージョン情報です。
LearnLean.lean
ライブラリのルートファイルです。ここから各モジュールを読み込んでいきます。
環境構築はここまでです。次回以降は、実際に Lean のコードを書きながら学習過程を記録していきます。
0 件のコメント:
コメントを投稿