From d273db183388c61feeb74413954fa9f93ed71933 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Fri, 13 Oct 2023 00:02:01 +0900 Subject: [PATCH 1/4] =?UTF-8?q?lean-ja=20=E3=81=AE=20discord=20=E3=81=A8?= =?UTF-8?q?=20zenn=20=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 団体紹介用のページを作る さらにメールアドレスの存在も示唆する --- content/_index.md | 6 ------ content/about.md | 13 +++++++++++++ 2 files changed, 13 insertions(+), 6 deletions(-) create mode 100644 content/about.md diff --git a/content/_index.md b/content/_index.md index daf452d..13ad9ed 100644 --- a/content/_index.md +++ b/content/_index.md @@ -16,9 +16,3 @@ Lean は証明支援系でもあり，数学の証明を検証する能力を備 現在，Lean で数学理論を実装していこうという努力が積極的に行われています．[mathlib4](https://github.com/leanprover-community/mathlib4) というライブラリがあり，大学の学部程度の数学のかなりの部分を Lean で行うことが可能になっています． [Lean 4 Web](https://lean.math.hhu.de/) から Lean を試すことができます．あなたも Lean で新しい数学を体験してみませんか？ - -## __わたしたちについて__ - -lean-ja は，Lean に関する情報の交換と集積を目的とした日本語コミュニティです．[discussion](https://github.com/orgs/lean-ja/discussions)でLeanに関する情報を日本語でやり取りすることができます．質問やアイデア共有などにぜひお使いください． - -また，Leanの学習リソースの翻訳を順次ホスト・公開する予定です． \ No newline at end of file diff --git a/content/about.md b/content/about.md new file mode 100644 index 0000000..91810fc --- /dev/null +++ b/content/about.md @@ -0,0 +1,13 @@ ++++ +title = "About" +description = "私たちについて" +weight = 2 ++++ + +lean-ja は，Lean に関する情報の交換と集積を目的とした日本語コミュニティです． + +お問い合わせは [GitHub](https://github.com/lean-ja) に記載のメールアドレスからお願いします． + +* [Discussion](https://github.com/orgs/lean-ja/discussions) +* [Discord](https://discord.gg/p32ZfnVawh) +* [Zenn](https://zenn.dev/leanja) From 8a2d8526a56146a1e1c92866db73b0d90f75678f Mon Sep 17 00:00:00 2001 From: Seasawher Date: Fri, 13 Oct 2023 00:02:26 +0900 Subject: [PATCH 2/4] =?UTF-8?q?math=20in=20type=20theory=20=E3=81=AE?= =?UTF-8?q?=E3=83=AA=E3=83=B3=E3=82=AF=E3=82=92=20Zenn=20=E3=81=AB?= =?UTF-8?q?=E5=A4=89=E6=9B=B4=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- content/links.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/links.md b/content/links.md index a98d77c..29c49f1 100644 --- a/content/links.md +++ b/content/links.md @@ -28,7 +28,7 @@ weight = 1 ## 日本語リソース * [Theorem Proving in Lean 4 日本語訳](https://aconite-ac.github.io/theorem_proving_in_lean4_ja/) Theorem Proving in Lean 4 の有志による日本語訳です． -* [Mathematics in type thoery 日本語訳](https://lean-ja.github.io/math-in-type-theory-ja/) Xena の記事「Mathematics in type theory」の非公式日本語訳です +* [Mathematics in type thoery 日本語訳](https://zenn.dev/leanja/articles/math_in_type_theory) Xena の記事「Mathematics in type theory」の非公式日本語訳です * [Leanのインストール方法・elanとLakeの使い方](https://aconite-ac.github.io/how_to_install_lean/) Leanのインストール方法・elanとLakeの使い方をまとめた有志による資料． * [数学系のためのLean勉強会](https://haruhisa-enomoto.github.io/lean-math-workshop/) 2023/09/03 に開催された，数学ユーザに向けたLean言語の勉強会．資料が公開されています． * [Lean4 タクティク逆引きリスト](https://lean-ja.github.io/tactic-cheetsheet/) 主なタクティクを使用場面から逆引きできるようにまとめたリストです． From c5b9d31a6397708022f225195c2f160db15d8ee4 Mon Sep 17 00:00:00 2001 From: Kitamado <47292598+Seasawher@users.noreply.github.com> Date: Fri, 13 Oct 2023 21:37:56 +0900 Subject: [PATCH 3/4] Update content/about.md Co-authored-by: aconite <140750505+aconite-ac@users.noreply.github.com> --- content/about.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/about.md b/content/about.md index 91810fc..8ce7943 100644 --- a/content/about.md +++ b/content/about.md @@ -8,6 +8,6 @@ lean-ja は，Lean に関する情報の交換と集積を目的とした日本 お問い合わせは [GitHub](https://github.com/lean-ja) に記載のメールアドレスからお願いします． -* [Discussion](https://github.com/orgs/lean-ja/discussions) +* [Discussion](https://github.com/orgs/lean-ja/discussions) : Leanに関する情報を日本語でやり取りすることができます．質問やアイデア共有などにぜひお使いください． * [Discord](https://discord.gg/p32ZfnVawh) * [Zenn](https://zenn.dev/leanja) From 206ca3ed47d9c9f0e3ff491d14613dd27655abdd Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 14 Oct 2023 23:23:26 +0900 Subject: [PATCH 4/4] =?UTF-8?q?GitHub=20Discussion=20=E3=81=AB=E3=81=AF?= =?UTF-8?q?=E8=AA=AC=E6=98=8E=E3=82=92=E8=BF=BD=E5=8A=A0=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- content/about.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/content/about.md b/content/about.md index 8ce7943..c6abfc3 100644 --- a/content/about.md +++ b/content/about.md @@ -8,6 +8,7 @@ lean-ja は，Lean に関する情報の交換と集積を目的とした日本 お問い合わせは [GitHub](https://github.com/lean-ja) に記載のメールアドレスからお願いします． -* [Discussion](https://github.com/orgs/lean-ja/discussions) : Leanに関する情報を日本語でやり取りすることができます．質問やアイデア共有などにぜひお使いください． +Lean に関する質問や相談を [GitHub Discussion](https://github.com/orgs/lean-ja/discussions) にて受け付けているほか，以下のような SNS でも活動しています． + * [Discord](https://discord.gg/p32ZfnVawh) * [Zenn](https://zenn.dev/leanja)