Update c1_introduction.md

軽微な文章の修正

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
-でどのように実装されているかについてお話しようと思います．
+でどのように実装されているかについてお話しようと思います．