リンク集更新

see:
Hitchhikers Guide をリンク集に追加する #554
リンク集に LeanSearch を追加する #548
MoogleにはVSCode拡張もある #549

src/links.md

@@ -1,6 +1,6 @@
 # リンク集
 
-## コミュニティ
+## 🌐 コミュニティ
 
 * [Lean Theorem Prover](https://leanprover.github.io/) Lean の公式サイト。
 * [Lean Community](https://leanprover-community.github.io/) Lean のユーザコミュニティ。
@@ -9,29 +9,34 @@
 * [Lean Forward](https://lean-forward.github.io/) 数学への Lean の応用を推進するコミュニティ。
 * [lean-ja](https://discord.gg/p32ZfnVawh) この資料を作っている lean-ja のディスコードサーバです。
 
-## ライブラリやツール
+## 🧰 ライブラリやツール
 
 * [Mathlib4](https://github.com/leanprover-community/mathlib4) Lean で大学の学部程度の数学を実装したライブラリ。
 * [Lean4 VSCode 拡張機能](https://github.com/leanprover/vscode-lean4) Lean4 のための VSCode 拡張機能。
-* [Loogle](https://loogle.lean-lang.org/) Mathlib の検索ツール。
-* [Moogle](https://www.moogle.ai/) 自然言語で Mathlib から定理や定義が検索できるツール。
-* [Chrome Lean Unicode](https://github.com/arthurpaulino/chrome-lean-unicode) Lean の VSCode 拡張機能が備える、Unicode 入力機能を Chrome で使えるようにする拡張機能。
+* [Loogle](https://loogle.lean-lang.org/) Mathlib の検索ツール。型の情報や定数名から検索ができます。vscode-lean4 から実行することもできます。
+* [Moogle](https://www.moogle.ai/) 自然言語で Mathlib から定理や定義が検索できるサイト。VSCode 拡張機能もあります。
+* [Lean Search](https://leansearch.net/) 自然言語で Mathlib から定理や定義が検索できるサイト。これに関連して[「A Semantic Search Engine for Mathlib4」](https://arxiv.org/abs/2403.13310)という論文があります。
 * [Lean4 Web](https://live.lean-lang.org/) ブラウザ上で Lean が実行できるプレイグラウンド。
 * [Reservoir](https://reservoir.lean-lang.org/) Lean 公式のパッケージレジストリ。
 
-## ドキュメントや教材
+## 📖 書籍
 
-* [Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4) Lean 4の定理証明支援系としての側面に焦点を当てた公式チュートリアルテキストです。
-* [Lean Manual](https://lean-lang.org/lean4/doc/) Lean 言語の公式ドキュメント。
+* [Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4) Lean 4の定理証明支援系としての側面に焦点を当てた公式チュートリアルテキストです。理論的な記述が多めです。
+* [Lean Manual](https://lean-lang.org/lean4/doc/) Lean 言語の公式ドキュメント。執筆中であり欠けている個所がいくつもあります。
 * [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/) 関数型プログラミング言語としての Lean の入門書。
-* [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) Lean でどのように数学を形式化するかを学ぶ教科書。初等整数論をはじめ、位相空間や測度も扱っています。
-* [Metaprogramming in Lean 4](https://leanprover-community.github.io/lean4-metaprogramming-book/) Lean で独自のコマンドやタクティクを作るための方法を解説した本。
+* [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) Lean で数学を形式化する方法を学ぶ教科書。初等整数論をはじめ、位相空間論や測度論も扱われるなど内容が充実しており、多くの演習問題があります。
+* [Metaprogramming in Lean 4](https://leanprover-community.github.io/lean4-metaprogramming-book/) Lean で独自のコマンドやタクティクを作る方法を解説した本。
+* [The Mechanics of Proof](https://hrmacbeth.github.io/math2001/) 大学の初級レベルの授業のための Lean を使った教科書。Mathlib にはない独自のタクティクが使用されていることに注意が必要です。
+* [The Hitchhiker's Guide to Logical Verification](https://github.com/blanchette/interactive_theorem_proving_2024) 「	Formal Proof and Verification」という授業の参考書。テーマは形式検証であり、形式数学の形式化だけでなくプログラミング意味論にも触れています。
+
+## 📝 書籍以外の参考資料
+
+* [Lean phrasebook](https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=0) 数学でのよくある推論ステップが、Lean にどのように翻訳されるかがよくまとめられたリストです。
 * [Natural Number Game 4](https://adam.math.hhu.de/#/g/leanprover-community/NNG4) Lean を使い、ペアノの公理から始めて自然数の基本的な性質を証明する初心者向けブラウザゲーム。
 * [Courses using Lean](https://leanprover-community.github.io/teaching/courses.html) Lean を題材とした講義のリスト。
-* [Lean phrasebook](https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=0) 数学でのよくある推論ステップが、Lean にどのように翻訳されるかがよくまとめられたリストです。
 
-## 日本語の資料
+## 🗾 日本語の資料
 
 * [Theorem Proving in Lean 4 日本語訳](https://aconite-ac.github.io/theorem_proving_in_lean4_ja/) Lean で数学の証明を行う方法を解説した公式チュートリアルの、有志による日本語訳です。
-* [数学系のためのLean勉強会](https://github.com/yuma-mizuno/lean-math-workshop) Lean で数学をどのように実装するのか、実際に実装する過程を追うことで学べる教材です。いくつかコード例を拝借させていただきました。
+* [数学系のためのLean勉強会](https://github.com/yuma-mizuno/lean-math-workshop) Lean で数学をどのように実装するのか、実際に実装する過程を追うことで学べる教材です。
 * [Leanのインストール方法・elanとLakeの使い方](https://aconite-ac.github.io/how_to_install_lean/) Leanのインストール方法・elanとLakeの使い方をまとめた有志による資料。