From 269cbc4eae7ff90433bda3b67b9e4124d739d25f Mon Sep 17 00:00:00 2001
From: Kitamado <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 8 Sep 2023 20:39:30 +0900
Subject: [PATCH] Update c1_introduction.md
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

軽微な文章の修正
---
 src/c1_introduction.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/c1_introduction.md b/src/c1_introduction.md
index 16cbe79..64744b9 100644
--- a/src/c1_introduction.md
+++ b/src/c1_introduction.md
@@ -43,7 +43,7 @@ $G$ が $x^5=x^8=1$ を満たす要素 $x$ によって生成される群だと
 群論をより深く理解している人なら，即座にこの群が自明であることがわかるでしょう．
 何が起こっているのかについて，はるかに洗練されたモデルを有しているからです．
 アイデアは複雑で，人によって異なるものです．
-「群が何であるか」という問いについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．
+「群とは何であるか」という問いについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．
 現在コンピュータは新しい定理を自力で証明することを苦手としていますが，その理由のひとつがこれです．
 コンピュータに群に関する定理を教えたり，群の例を教えたり，群論の定理や群の例を自動的に理解する AI
 を作ったりすることで，コンピュータの直感を発達させることができます．
@@ -52,4 +52,4 @@ $G$ が $x^5=x^8=1$ を満たす要素 $x$ によって生成される群だと
 写像が canonical (正準) であるという概念は，定義というよりむしろアイデアだと思います．
 数学者によって，このイタチごっこのような言葉に対する考え方は違ってくるでしょう．
 この記事では，他の３つの概念 (定義，命題，証明) が型理論や Lean theorem prover
-でどのように実装されているかについてお話しようと思います．
\ No newline at end of file
+でどのように実装されているかについてお話しようと思います．