deploy: 82bbc98

c1_introduction.html

@@ -166,14 +166,15 @@ <h1 class="menu-title">Mathematics in type theory 日本語版</h1>
                     <main>
                         <h1 id="イントロダクション"><a class="header" href="#イントロダクション">イントロダクション</a></h1>
 <!-- What is maths? I think it can basically be classified into four types of thing. There are definitions, true/false statements, proofs, and ideas. -->
-<p>数学とは何でしょうか？基本的に４つのタイプに分類できると思う．定義，命題，そしてアイデアです．</p>
+<p>数学とは何でしょうか？数学は基本的に４つのタイプに分類できると思います．
+定義，命題，証明，そしてアイデアです．</p>
 <!-- **Definitions** (for example the real numbers, or $\pi$) and **true/false statements** (for example the statement of Fermat’s Last Theorem or the statement of the Riemann Hypothesis) are part of the science of mathematics: these are black and white things which have a completely rigorous meaning within some foundational system. -->
 <p><strong>定義</strong> (たとえば実数や $\pi$) や<strong>命題</strong> (たとえばフェルマーの最終定理やリーマン仮説のステートメント)
 は数学の科学の一部です：こういったものは，ある基礎的なシステムの中で完全に厳密な意味を持ち，
 白黒はっきりしています．</p>
 <!-- **Proofs** are in some sense the currency of mathematics: proofs win prizes. Constructing them is an art, checking them is a science. This explains, very simply, why computer proof verification systems such as Lean, Coq, Isabelle/HOL, Agda… are much better at checking proofs than constructing them. -->
 <p><strong>証明</strong>はある意味で数学の通貨だといえます：証明は賞で報いられます．証明の構築は芸術であり，
-それを検証するのは科学です．このことは，Lean, Coq, Isabelle/HOL, Agda
+証明の検証は科学です．このことは，Lean, Coq, Isabelle/HOL, Agda
 などのコンピュータ証明検証システムが，証明を構築するよりもチェックすることをはるかに得意とする理由を，
 とても簡単に説明しています．</p>
 <!-- And **ideas** are the purely artistic part of mathematics. That “lightbulb” moment, the insight which enables you to solve a problem — this is the elusive mathematical idea. -->
@@ -199,15 +200,15 @@ <h1 id="イントロダクション"><a class="header" href="#イントロダク
 群論をより深く理解している人なら，即座にこの群が自明であることがわかるでしょう．
 何が起こっているのかについて，はるかに洗練されたモデルを有しているからです．
 アイデアは複雑で，人によって異なるものです．
-群が何であるかについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．
+「群とは何であるか」という問いについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．
 現在コンピュータは新しい定理を自力で証明することを苦手としていますが，その理由のひとつがこれです．
 コンピュータに群に関する定理を教えたり，群の例を教えたり，群論の定理や群の例を自動的に理解する AI
 を作ったりすることで，コンピュータの直感を発達させることができます．
 しかし直感というのはとても微妙なもので，私にはまったく理解できないので，
 ここではこういったアイデアについてはこれ以上語らないことにします．
 写像が canonical (正準) であるという概念は，定義というよりむしろアイデアだと思います．
 数学者によって，このイタチごっこのような言葉に対する考え方は違ってくるでしょう．
-この記事では，他の３つの概念が型理論や Lean theorem prover
+この記事では，他の３つの概念 (定義，命題，証明) が型理論や Lean theorem prover
 でどのように実装されているかについてお話しようと思います．</p>
 
                     </main>

print.html

@@ -176,14 +176,15 @@ <h2 id="この翻訳について"><a class="header" href="#この翻訳につい
 <p>翻訳に際して，機械翻訳サービス<a href="https://www.deepl.com/ja/translator">DeepL翻訳</a>を参考にしました．</p>
 <div style="break-before: page; page-break-before: always;"></div><h1 id="イントロダクション"><a class="header" href="#イントロダクション">イントロダクション</a></h1>
 <!-- What is maths? I think it can basically be classified into four types of thing. There are definitions, true/false statements, proofs, and ideas. -->
-<p>数学とは何でしょうか？基本的に４つのタイプに分類できると思う．定義，命題，そしてアイデアです．</p>
+<p>数学とは何でしょうか？数学は基本的に４つのタイプに分類できると思います．
+定義，命題，証明，そしてアイデアです．</p>
 <!-- **Definitions** (for example the real numbers, or $\pi$) and **true/false statements** (for example the statement of Fermat’s Last Theorem or the statement of the Riemann Hypothesis) are part of the science of mathematics: these are black and white things which have a completely rigorous meaning within some foundational system. -->
 <p><strong>定義</strong> (たとえば実数や $\pi$) や<strong>命題</strong> (たとえばフェルマーの最終定理やリーマン仮説のステートメント)
 は数学の科学の一部です：こういったものは，ある基礎的なシステムの中で完全に厳密な意味を持ち，
 白黒はっきりしています．</p>
 <!-- **Proofs** are in some sense the currency of mathematics: proofs win prizes. Constructing them is an art, checking them is a science. This explains, very simply, why computer proof verification systems such as Lean, Coq, Isabelle/HOL, Agda… are much better at checking proofs than constructing them. -->
 <p><strong>証明</strong>はある意味で数学の通貨だといえます：証明は賞で報いられます．証明の構築は芸術であり，
-それを検証するのは科学です．このことは，Lean, Coq, Isabelle/HOL, Agda
+証明の検証は科学です．このことは，Lean, Coq, Isabelle/HOL, Agda
 などのコンピュータ証明検証システムが，証明を構築するよりもチェックすることをはるかに得意とする理由を，
 とても簡単に説明しています．</p>
 <!-- And **ideas** are the purely artistic part of mathematics. That “lightbulb” moment, the insight which enables you to solve a problem — this is the elusive mathematical idea. -->
@@ -209,15 +210,15 @@ <h2 id="この翻訳について"><a class="header" href="#この翻訳につい
 群論をより深く理解している人なら，即座にこの群が自明であることがわかるでしょう．
 何が起こっているのかについて，はるかに洗練されたモデルを有しているからです．
 アイデアは複雑で，人によって異なるものです．
-群が何であるかについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．
+「群とは何であるか」という問いについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．
 現在コンピュータは新しい定理を自力で証明することを苦手としていますが，その理由のひとつがこれです．
 コンピュータに群に関する定理を教えたり，群の例を教えたり，群論の定理や群の例を自動的に理解する AI
 を作ったりすることで，コンピュータの直感を発達させることができます．
 しかし直感というのはとても微妙なもので，私にはまったく理解できないので，
 ここではこういったアイデアについてはこれ以上語らないことにします．
 写像が canonical (正準) であるという概念は，定義というよりむしろアイデアだと思います．
 数学者によって，このイタチごっこのような言葉に対する考え方は違ってくるでしょう．
-この記事では，他の３つの概念が型理論や Lean theorem prover
+この記事では，他の３つの概念 (定義，命題，証明) が型理論や Lean theorem prover
 でどのように実装されているかについてお話しようと思います．</p>
 <div style="break-before: page; page-break-before: always;"></div><!-- # Definitions, true/false statements, and proofs -->
 <h1 id="定義命題証明"><a class="header" href="#定義命題証明">定義，命題，証明</a></h1>