数学系エンドユーザーのためのLean入門

「数学系エンドユーザーのためのLean入門」の講義資料です．

• 講義概要:
  • https://www.math.kyoto-u.ac.jp/ja/event/seminar/6028
• 講義資料:
  • https://shosonoda.github.io/lean-math-note/
  • https://github.com/shosonoda/lean-math-note/
• 環境構築:
  • https://shosonoda.github.io/lean-install/
• 担当:
  • 園田翔（理化学研究所 / サイバーエージェント）
• Lean version:
  • leanprover/lean4:v4.30.0

使い方

GitHubリポジトリをローカルに clone

git clone https://github.com/shosonoda/lean-math-note.git

プロジェクトルートで Lean バージョン確認

cd lean-math-note
cat lean-toolchain
elan show | grep -A 5 "active toolchain"

キャッシュ取得後，ビルド

lake exe cache get
lake build

VS Code 起動

code .