Merge pull request #23 from lean-ja/add-social-info

メールアドレス，Discord, Zenn を追加する

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の学習リソースの翻訳を順次ホスト・公開する予定です．

content/about.md

@@ -0,0 +1,14 @@
++++
+title = "About"
+description = "私たちについて"
+weight = 2
++++
+
+lean-ja は，Lean に関する情報の交換と集積を目的とした日本語コミュニティです．
+
+お問い合わせは [GitHub](https://github.com/lean-ja) に記載のメールアドレスからお願いします．
+
+Lean に関する質問や相談を [GitHub Discussion](https://github.com/orgs/lean-ja/discussions) にて受け付けているほか，以下のような SNS でも活動しています．
+
+* [Discord](https://discord.gg/p32ZfnVawh)
+* [Zenn](https://zenn.dev/leanja)

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/) 主なタクティクを使用場面から逆引きできるようにまとめたリストです．