From 32ceb38a2e91329e76b0a64081baacf98a97daa8 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 13 Oct 2024 20:33:14 +0900 Subject: [PATCH] =?UTF-8?q?=E3=83=AA=E3=83=B3=E3=82=AF=E3=81=AE=E4=BF=AE?= =?UTF-8?q?=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- booksrc/links.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/booksrc/links.md b/booksrc/links.md index 8a858a95..3d44521e 100644 --- a/booksrc/links.md +++ b/booksrc/links.md @@ -20,7 +20,7 @@ * [Lean4 VSCode 拡張機能](https://github.com/leanprover/vscode-lean4) Lean4 のための VSCode 拡張機能。 * [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)という論文があります。 +* [Lean Search](https://leansearch.net/) 自然言語で Mathlib から定理や定義が検索できるサイト。これに関連して[「A Semantic Search Engine for Mathlib4」](https://www.semanticscholar.org/paper/A-Semantic-Search-Engine-for-Mathlib4-Gao-Ju/da6bf364987a605843d56b19f9d0b1546b192c5f?utm_source=direct_link)という論文があります。 * [Lean4 Web](https://live.lean-lang.org/) ブラウザ上で Lean が実行できるプレイグラウンド。 * [Reservoir](https://reservoir.lean-lang.org/) Lean 公式のパッケージレジストリ。