Xena 日本語訳

この文書は，Kevin Buzzard 氏によるブログ Xena の記事のいくつかを日本語訳したものです．

この翻訳について

この翻訳は有志による非公式翻訳です．翻訳に際して，表現を大きく変えた箇所があります．また, 用語の訳が一般的でない可能性があります．誤りを含む可能性もあります．ご了承ください．

原著者より翻訳および公開の許可はいただいていますが，訳文を確認していただいているわけではなく，本文に誤りがあればそれはすべて訳者の責任です．

また，原文の記事の古さに起因する誤りがある可能性があります．

誤字脱字，内容の誤りの指摘，翻訳の改善の提案を歓迎いたします．GitHubリポジトリまでお寄せください．

翻訳に際して，機械翻訳サービスDeepL翻訳を参考にしました．

Mathematics in type thoery 日本語訳

原文は Mathematics in type theory. です．

イントロダクション

数学とは何でしょうか？数学は基本的に４つのタイプに分類できると思います．定義，命題，証明，そしてアイデアです．

定義 (たとえば実数や $\pi$) や命題 (たとえばフェルマーの最終定理やリーマン仮説のステートメント) は数学の科学の一部です：こういったものは，ある基礎的なシステムの中で完全に厳密な意味を持ち，白黒はっきりしています．

証明はある意味で数学の通貨だといえます：証明は賞で報いられます．証明の構築は芸術であり，証明の検証は科学です．このことは，Lean, Coq, Isabelle/HOL, Agda などのコンピュータ証明検証システムが，証明を構築するよりもチェックすることをはるかに得意とする理由を，とても簡単に説明しています．

そしてアイデアは，数学の純粋に芸術的な部分です．「閃き」の瞬間，問題解決を可能にする洞察力，これこそが数学のとらえどころのないアイデアなのです．

アイデアは，形式的な意味で私が最も理解していない数学の一部です．ここに２つの疑問があります：

群とは何ですか？

群をどう考えていますか？

最初のものは正確な「科学的な」質問です．群とは，ある特別な構造を持ち，ある公理を満たす集合のことです．正式な答えは Wikipediaの群についてのページにあります．群とは定義です．しかし，２つめの質問は種類の異なる質問です．群について考える方法は人によって異なります．$G$ が $x^5=x^8=1$ を満たす要素 $x$ によって生成される群だとします．$G$ について何が言えるでしょうか？もしあなたが数学の学部生で，群の形式的な定義を見たばかりなら，おそらく何も言えないでしょう．群論をより深く理解している人なら，即座にこの群が自明であることがわかるでしょう．何が起こっているのかについて，はるかに洗練されたモデルを有しているからです．アイデアは複雑で，人によって異なるものです．「群とは何であるか」という問いについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．現在コンピュータは新しい定理を自力で証明することを苦手としていますが，その理由のひとつがこれです．コンピュータに群に関する定理を教えたり，群の例を教えたり，群論の定理や群の例を自動的に理解する AI を作ったりすることで，コンピュータの直感を発達させることができます．しかし直感というのはとても微妙なもので，私にはまったく理解できないので，ここではこういったアイデアについてはこれ以上語らないことにします．写像が canonical (正準) であるという概念は，定義というよりむしろアイデアだと思います．数学者によって，このイタチごっこのような言葉に対する考え方は違ってくるでしょう．この記事では，他の３つの概念 (定義，命題，証明) が型理論や Lean theorem proverでどのように実装されているかについてお話しようと思います．

定義，命題，証明

アイデアとは対照的に，数学の他の部分（定義，定理/予想, 証明）は基礎的なシステムで形式化することができ，したがって精確な方法でコンピュータ上に作成・保存することができます．これは pdf ファイルのことではありません！pdf ファイルこそ，私が脱却したいものなのです！つまり，様々ある数学の基礎付け（集合論，型理論，圏論）のうち1つを理解するコンピュータプログラミング言語が設計されており，その言語で数学者が問題の定義，命題，証明を書くことができるということです．

私には，圏論でどのように数学の基礎付けを行うのかを説明する資格はありません．集合論について，ひとつだけ観察してみましょう．集合論における定義，たとえば実数や $\pi$ の定義は集合です．そして証明とは，論理のステップをつなげたものです．集合論において，定義と証明は全く異なるもののように私には思えます．群とは，定義と証明の混合物です．―― 群とは，順序付き4つ組 $(G,m,i,e)$ であって，特定の公理を満たすもののことです．つまり，論理が付属した集合です．

しかし，型理論では驚くほど違います．今挙げた３つのもの ―― 定義，命題，証明 ―― はすべて同じ種類のものです！これらはすべて項です．群，証明，実数 ―― これらもすべて項です．定義と証明の統一，つまり集合と論理の統一が，型理論を実用的な基礎システムたらしめ，コンピュータに学部レベルのすべての数学を教えることを可能にしています．

宇宙，型，項

型理論では，すべてが項です．そしていくつかの項は型でもあります．すべての項が型であるわけではありませんが，すべての項は型を持っています．Lean では，コロンを使って項の型を表します．―― x : T という表記で，x が T という型の項であることを表します．たとえば，実数 $\pi$ は Lean の項であり，実数全体 $\mathbb{R}$ は型であり，π : ℝ が成り立ちます．つまり，$\pi$ は型 $\mathbb{R}$ の項です．集合論では $\pi\in\mathbb{R}$ と書きますが，型理論では π : ℝ と書きます．どちらも同じ数学的概念，つまり「$\pi$ は実数である」を表します．

いま $\pi$ は項ですが，型ではありません. Lean では x : π は意味を持ちません．集合論では，$x\in\pi$ は意味を持ちますが，これは集合論において全てが集合であることに起因する，奇妙な偶然です．さらに，$\pi$ の実際の要素は，実数がどのように実装されるか（たとえばデデキント切断としてか，コーシー数列としてか）に依存するため，集合論での $x\in\pi$ は，構文的には意味を持つものの，数学的な意味はありません．たまたま意味をなすだけで，システムの癖に過ぎません．もし「 $x \in \pi$ には意味があるはずだ」とあなたが断固として言うなら，「あなたは集合論に洗脳されているのだ」と私は言うでしょう．ガウスとオイラーがあなたを正しい方向に導いてくれるでしょう：ガウスとオイラーは，コーシーとデデキントが数列と切断を導入する以前に，実数に関する定理を証明していました．$\pi$ が要素を持つべき理由はありません．これは数学の基礎に集合論を使った際の癖であり，その癖は型理論を使った場合には解消されます．

先ほど，すべての項は型を持つと書きました．では ℝ の型はなんでしょうか？ℝ : Type が答えです．実数全体は，Type と呼ばれる「宇宙」型の項です ―― これは「すべての集合がなすクラス」の型理論における類似物です．

数学者が定義する数学的対象の多くは，型 Type を持つか，あるいは T : Type であるような型 T を持ちます．漠然とした経験則ですが，要素を持つもの（群，環，体など）は Type 型を持ち，要素を持たないもの（$\pi$, $\sqrt{2}$ や一般の群の要素 $g$）は T 型を持ちます．もう一つのあいまいな経験則として，大文字で書くもの（群や環など）や fancy letter（実数 ℝ や有理数 ℚ ）で書くものは Type 型を持ち，小文字で書くもの（群の要素 $g$ や実数 $r$, 整数 $n$）は T 型を持つ傾向にあります．たとえば 2 : ℕ と ℕ : Type が成り立ちます．また $g$ が群 $G$ の要素であるとき，Lean では g : G と G : Type が成り立ちます．ここには３層の階層があります ―― 一番下に項があり，その上に型があり，最上部に宇宙があります．

宇宙 : Type

具体的な型 : ℝ, ℕ, G (群), R (環), X (集合論者が集合と呼ぶなにか), バナッハ空間など. 形式的には ℝ : Type などと書きます.

具体的な項 : π (型 ℝ の項), g (群 G の要素, つまり型 G の項), x (X の要素, つまり型 X の項). 形式的には g : G などと書きます.

この階層は，クラス（たとえばすべての集合のクラス）と集合の２つのレベルしかない集合論の階層よりも，表現力が高いです．

数学におけるコロンの標準的な使い方があります．―― 関数を書くための記法です．X と Y が集合（集合論を使っている場合）または型（型理論を使っている場合）であるとき，X から Y への関数を f : X → Y と書きます．これは実は Lean におけるコロンの使い方と一致しています．X から Y への関数の集まり $\mathrm{Hom}(X,Y)$ に対する Lean の表記法は X → Y であり，これは型です．（つまり X → Y : Type です．これは集合論で $\mathrm{Hom}(X,Y)$ を集合と考えることに対応しています）f : X → Y は f が X → Y 型の項であることを意味し．集合論でいう $f \in \mathrm{Hom}(X,Y)$ に対応します．これは型理論において，f が X から Y への関数であることを書き表すやり方です．

（これは試験に出ません）厳密に言えば，宇宙は型であり，型は項ですが，これは用語の問題です．多くの場合，ひとが型について語るとき，それは宇宙ではない型を意味し，ひとが項について語るとき，それは型ではない項を意味します．しかし常にそうとは限りません．私が初心者の頃は，これで混乱しました．

定理と証明

ここからが楽しいところです．ここまで，型とは型理論における集合の呼び名であり，項とは型理論における要素の呼び名でした．しかし，ここで Lean の型理論におけるもう一つの宇宙，命題の宇宙 Prop を見てみましょう．そこで起こることは，私たちの伝統的なメンタルモデルとは全く異なります．ここでは，定理のステートメントと証明が，型や項と同じようにどのようにモデル化できるかを見ていきます．

定理のステートメントと証明はどのようにモデル化されるのでしょうか？Lean の型理論には Type という宇宙だけでなく，Prop という第二の宇宙があります．Prop 型の項は命題です．ここで残念な表記の衝突があります．数学では，proposition (命題)という言葉はしばしば定理のこどもという意味で使われますが，定理は真です．（そうでなければ予想や反例と呼ばれます）したがって，数学において命題という言葉は真である文を指しますが，ここでは，論理学者と同じように命題という言葉を使います．つまり，命題とは一般的な真か偽かどちらかになる文のことであり，それが正しいか誤りかは関係ありません．

例を見るとわかりやすいでしょう．$2 + 2 = 4$ は命題なので 2 + 2 = 4 : Prop と書くことができます．しかし，$2 + 2 = 5$ も命題なので，2 + 2 = 5 : Prop と書くこともできます．何度も言いますが，命題が真である必要はありません！命題は真か偽かどちらかになる文のことです．もう少し複雑な例を見てみましょう．

「すべての自然数 $x$ について $x + 0 = x$ である」という文は命題です．Lean では，これは (∀ x : ℕ, x + 0 = x) : Prop と表せます．命題は Prop 型を持つ項です．（先ほど見てきた項が型 Type を持っていたのと同様です）RH をリーマン仮説のステートメントとします．すると RH : Prop となります．それが真か偽か，特定の数学の公理と独立であるか，決定不能であるか，等は問いません．命題とは真か偽かどちらかになる文のことです．Lean の型理論の階層のうち，Prop 宇宙に住む部分を見てみましょう．

宇宙 : Prop

具体的な型 : 2 + 2 = 4, 2 + 2 = 5, フェルマーの最終定理のステートメント，リーマン仮説のステートメント

具体的な項 : ??

この３層構造の Prop 階層において，項にあたるものは何でしょうか？それは証明です！

命題は型，証明は項

これは，型理論の世界と集合論の世界との，そして３年前までの私の脳内世界との大きく異なる点です．何が起こっているのか理解しようとして，私は数学者が用語の濫用を行っていることに気づきました．まずそれについて考えてみましょう．ボルツァーノ＝ワイエルシュトラスの定理とは, 解析学における, 収束する部分列を持つ有界数列についてのステートメントです．数学者が「ボルツァーノ＝ワイエルシュトラスの定理」という言葉を実際にどのように使うかについて，少しお話ししましょう．数学者は，「ボルツァーノ＝ワイエルシュトラスの定理とは，収束する部分列を持つ数列に関するこのステートメントのことだ」と言うでしょう．しかし証明の途中で，証明を続けるためにこの定理を適用する必要がある場合は，「ボルツァーノ＝ワイエルシュトラスの定理によって，収束する部分列があることが推論される」と言います．何もおかしなことはないように思えます．しかし，私が指摘したいのは，「ボルツァーノ＝ワイエルシュトラスの定理」という言葉が２つの異なる意味で使われている，ということです．「ボルツァーノ＝ワイエルシュトラスの定理とは何か」という場合，かれらは定理のステートメントに言及しています．しかし，「ボルツァーノ＝ワイエルシュトラスの定理を使って」という場合，実際に使っているのはその証明です．バーチ・スウィンナートン＝ダイアー予想は，完全に整った命題であり，それが何であるかを正確に言うことができます．しかし，ある証明を完全なものにしたいのであれば，バーチ・スウィンナートン＝ダイアー予想をその証明の途中で使うことはできません．なぜなら現時点でこの予想は未解決問題だからです．ここで重要なのは，定理のステートメントと定理の証明とを明確に区別することです．数学者は「ボルツァーノ＝ワイエルシュトラスの定理」という言葉を，どちらの意味でも使うことがあります．このような非形式的な表記の濫用は初学者の混乱を招きます．なぜなら，以下では定理のステートメントと定理の証明を区別することが本当に重要だからです．この２つは全く異なるものです．

natural number game (自然数ゲーム) ¹の中で，私は数学者を相手にしていたのでこのような表記の濫用を行っていました．∀ x : ℕ, x + 0 = x という文は真であり，「これは Lean では add_zero と呼ばれる」と私は言っていました．natural number game において，私は add_zero : ∀ x : ℕ, x + 0 = x と書いていました．しかし，これが何を意味するかといえば，Lean で add_zero と呼ばれる項が ∀ x : ℕ, x + 0 = x の証明である，ということなのです！コロンは型理論的に使われています．私は natural number game では意図的にこの概念を曖昧にしました．add_zero はすべての $x$ に対して $x + 0 = x$ であるという「アイデア」と何らかの形で等しいと，数学者に信じさせたわけです．しかし裏では ∀ x : ℕ, x + 0 = x は命題であり，型でもあり，add_zero はその証明であり，項でもあります．ここで重要なのは，定理のステートメントとその証明を区別することです．ステートメントは型であり，証明は項です．

宇宙 : Prop

具体的な型 : 2 + 2 = 4, 2 + 2 = 37, フェルマーの最終定理 ∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0

具体的な項 : 2 + 2 = 4 の証明（2 + 2 = 4 型を持つ項），フェルマーの最終定理の証明（∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0 という型を持つ項）

¹ 訳注: natural number game は，ペアノの公理から始めて整数の基本的な性質を Lean で示すブラウザゲームです．ここで紹介されているのは Lean3 版ですが，Lean4 版がこちらにあります．ソースコードはこちらです．

定理の要素

つまり π : ℝ というステートメントに対する私たちのメンタルモデルは，型である ℝ は「ものの集まり」であり，項である π はその集まりのメンバーである，ということです．このアナロジーを続けるなら，2 + 2 = 4 というステートメントはある種の集まりであり，2 + 2 = 4 の証明はそのメンバーです．言い換えれば，Lean は 2 + 2 = 4 をある種の集合であるとし，2 + 2 = 4 の証明はその集合の要素であるとするようなモデルを提案しているのです．Lean では，ある命題の証明はすべて等しいという公理が組み込まれています．つまり a : 2 + 2 = 4 かつ b : 2 + 2 = 4 ならば a = b となります．これは Prop 宇宙の中だから起こることです ―― これが Lean における命題の振る舞いです．Type 宇宙の中ではこのようなことはありえません．―― π : ℝ かつ 37 : ℝ ですが，$\pi\not=37$ です．この Prop 宇宙の特別な癖は「proof irrelevance (証明無関係)」と呼ばれます．形式的には，P : Prop に対して a : P かつ b : P ならば a = b である，と言い表せます．もちろん，ある命題が偽ならば，その命題には証明は全くありません！偽の命題は空集合のようなものです．つまり，Lean の命題のモデルは，真の命題は１つの要素を持つ集合のようなもので，偽の命題は $0$ 個の要素を持つ集合のようなものだと言っています．

f : X → Y であるとき，f は X から Y への関数であるということを思い出しましょう．ここで，$P$ と $Q$ を命題とし，$P\implies Q$ がわかっているとします．これは何を意味するでしょうか？これは $P$ ならば $Q$ であるということを意味します．$P$ が真であるとき，$Q$ も真だということです．$P$ の証明があれば，$Q$ の証明も作れるということです．$P\implies Q$ は $P$ の証明から $Q$ の証明を得る関数です．$P$ の要素を $Q$ の要素に送る関数です．P → Q 型を持つ項です．繰り返しますが，$P\implies Q$ の証明は h : P → Q という項 h です．natural number game で，私が → 記号を含意を表すのに使ったのは，このためです．

false を一般的な偽の文（$0$ 個の要素を持つ集合と考えられる）とし，true を一般的な真の文（$1$ 個の要素を持つ集合と考えられる）とします．false → false 型の項，または true → true 型の項を作ることはできるでしょうか？もちろんです．―― 恒等関数を使えばよいだけです．実際，どちらの場合も関数は一意に定まります．―― hom 集合のサイズは $1$ です．false → true 型の項を作ることはできるでしょうか？もちろん，$0$ 個の要素を持つ集合から $1$ 個の要素を持つ集合への関数はあり，この関数も一意です．では true → false 型の項を作ることはできますか？これはできません．true の証明をどこに送ればいいのでしょうか？false の証明は存在しないので，送る先がありません．したがって true → false はサイズ $0$ の集合です．これは → の標準的な真理値表に相当し，最初に分析した３つの文は真で，最後の文は偽です．

フェルマーの最終定理の証明は関数

では ∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0 の証明とはどのようなものでしょうか？この命題には矢印が含まれているので，フェルマーの最終定理のステートメントは $\mathrm{Hom}(A,B)$ という形の集合の一種です．Lean では，フェルマーの最終定理の証明は実際に関数です！その関数が何をするかは次の通りです．それは４つの入力を持ちます．最初の３つの入力は自然数 x, y, z です．４番目の入力は証明で，命題 n > 2 ∧ x^n + y^n = z^n の証明です．そして出力は命題 x*y=0 の証明です．これは「フェルマーの最終定理の証明とは何か」という問いについてのきわめて型破りな考え方であり，証明を実際に理解しようとする際には全く役に立たないことを強調しておきましょう． ―― しかし，これは数学がどのように機能するかについての完全に一貫したメンタルモデルです．数と証明の概念を統一することで，―― つまり両方を項として考えることで，―― 証明を関数として考えることができます．Lean は関数型プログラミング言語であり，特に関数を中心に設計されています．現在 Lean や Coq や Isabelle/HOL といった型理論を使用する証明支援系が，Metamath や Mizar のような集合論を使用する証明支援系より進んでいるのは，このためだと私は確信しています．

定理を証明しましょう！関数を書きましょう！


宇宙	`Type`	`Prop`
型の例	ℝ	2 + 2 = 5, (∀ a : ℕ, a + 0 = a)
項の例	37, π	`add_zero`, `rfl`

Division by zero in type theory: a FAQ 日本語訳

原文は Division by zero in type theory: a FAQ です．

ねえ, Lean では 1/0＝0 だって聞いたんだけど, 本当？

本当ですよ．Coq や Agda，その他多くの証明支援系と同じです．

それは矛盾にならないの？

いいえ．Lean の $/$ 記号が数学的な割り算を意味しないというだけです．$\mathbb{R}$ を実数全体とします．関数 $f:\mathbb{R}^2\to\mathbb{R}$ を $y\not=0$ に対しては $f(x,y)=x/y$ であり，$y=0$ のとき $f(x,0)=0$ を満たすようなものとして定義します．この定義が数学に矛盾をもたらすでしょうか？もちろんそんなことはありません！単なる定義です．Lean は $/$ 記号を $f$ の意味で使います．Coq や Agda と同じようにです．この関数は Lean では実際には $f$ ではなく，real.div と呼ばれます．

でも，混乱しない？

確かに Twitter では混乱を招いているようですね．しかし，証明支援系で数学を行うときに混乱することはありません．数学者は0で割り算をしませんから，real.div と数学的割り算（1/0 は定義されない）の違いに気づくことはないのです．実際，Lean における 1/0 の定義を気にしている数学者がいたとしたら，その理由を尋ねられるでしょう．知っての通り，数学では 0 での割り算は許されていませんから，数学をする上では関係ないはずだからです．実のところ，real.div と数学的な割り算は同じと考えてよいものです．すべての real.div に関する定理は数学的な割り算に翻訳できますし，逆も然りです．real.div を実装することは，数学的な割り算を実装することと等価です．

こんな慣例ばかげてる！

ゼロ除算以外にも例があります．自然数 $\lbrace 0,1,2,\ldots \rbrace$ には引き算 nat.sub が定義されていて，x - y と書きます．これは2つの自然数を与えられたら1つの自然数を返します．仮に x < y だったとしたら，x - y は 0 です．real.sqrt という関数もあり，これは実数を1つ与えられたら実数を1つ返します．$2$ を入力したら出力は $\sqrt{2}$ です．-1 を入力したら，何が返されるかはよくわかりませんが実数が返ってくることは保証されています．$0$ かもしれませんし，$1$ かもしれません．$37$ かも? どうだっていいことです．私は数学者であり，負の実数の平方根を取りたい場合 real.sqrt は使いません．なぜなら実数で答えを出したくないからです．一方で real.sqrt の型は ℝ → ℝ です．

数学者がやるような常識的な方法では何がまずいの？

素晴らしい質問ですね．2017 年に私は試してみました．証明支援系ではとても不便な方法だということがわかりました！

私が Lean を学んでいたときのことです．私は「普通の数学者」として，学部の証明入門コースに Lean を取り入れようと考えていました．私は当時定理証明の経験がなく, プログラミングの正式な素養もありませんでした．Lean での授業が実現可能か調査するために，学部生に配る予定だった問題集をすべて Lean でやってみました．これは Lean の数学ライブラリがもっと小さくて，real.sqrt がまだ存在していなかった 2017 年当時の話です．しかし sup と inf の基本理論は形式化されていたので，私は 0 以上の x に対して real.sqrt x を $\mathrm{Sup}\lbrace y\in\mathbb{R} ∣ y^2\leq x\rbrace$ として定義しました．そして，平方根関数を扱うのに必要な $\sqrt{ab}=\sqrt{a}\sqrt{b}$ や $\sqrt{a^2}=a$ や $\sqrt{a^2b}=a\sqrt{b}$ などの基本的な定理を証明しました．(ここで $a, b$ は非負実数です．私の定義した平方根関数は非負実数しか受け付けません．)

そして私の授業の問題集にあった $\sqrt{2}+\sqrt{3}<\sqrt{10}$ に取り掛かりました．電卓を使わずに，代数的な操作だけを使って証明せよという問題です．つまり，real.sqrt を使う問題です．言うまでもなく，私が使った定義では，$\sqrt{\phantom{2}}$ を使うたびに毎回平方根の中が非負であることを証明する必要があります．毎度毎度平方根が現れるたびにです．たとえ前の行で 2 > 0 を証明していても，次の行で $\sqrt{2}$ があればまた示す必要があるのです．もちろん証明は norm_num で済むのですが，私はすぐにこれをタイプするのが嫌になりました．

Lean チャットでこのことを愚痴ったところ，数学者の慣習の愚かさを指摘され，Lean 流の慣用的なやり方を教えられました．それは，負の数のようなゴミ入力を平方根関数に許可し，ゴミ出力を返すことです．非負の仮定は定理の中に置きます．例えば，$\sqrt{ab}=\sqrt{a}\sqrt{b}$ という定理には, $a,b\geq 0$ であるという仮定を持たせます．$ab\geq 0$ という仮定は持たせないことに注意してください．というのも，証明の中で導くことができるので，この定理のユーザにそれを示させる必要がないからです．これは関数に仮定を持たせる数学者流のアプローチとは対照的です．数学者流では，$\sqrt{\phantom{2}}$ という表記自体が非負性を要求するので，$ab\geq 0$ も示す必要がありました．

じゃあ, このクレイジーなやり方の方が本当はいいってこと？

いや, そこまで言っていません．私が言っているのは，(a) 私たち数学者が現在行っていることと数学的に同等であり，(b) 従属型理論で数学を形式化する際に，単純により便利であるということです．

体とは何かを考えてみましょう．数学では，体とは $0,1,a+b,-a,a\times b,a^{-1}$ を持つ集合 $F$ のことです．ただし逆元を取る操作 $a^{-1}$ はゼロでない $a$ に対してのみ定義されます．体のゼロでない要素は群を形成し，$x\not=0$ に対して $x\times x^{-1}=1$ という公理を満たします．($x = 0$ のときこれは意味をなしません)ここで我々が異星人と遭遇し，その異星人も体を発見していたとしましょう．しかし異星人の定義では，$x^{-1}$ ではなく関数 $\iota :F\to F$ を使用していたとします．その $\iota$ は，我々の表記法を用いると $x\not=0$ のとき $\iota(x)=x^{-1}$ で，$\iota(0)=0$ を満たすとします．もちろん異星人の公理は我々のものと同じで，たとえば $x\not=0$ に対して $x\times \iota(x)=1$ が成り立っています．異星人の体は追加の公理 $\iota(0)=0$ を持っていますが，これは大きな問題にはなりません．一長一短です．ーー異星人流には $a/b:=a\times\iota(b)$ と定義され，彼らの定理 $(a+b)/c=a/c+b/c$ には我々が必要とするような $c\not=0$ という仮定が必要ありません．同じアイデアを表現するために，少し違った表記を使っているだけなのです．異星人の $\iota$ は不連続です．我々のは体全体で定義されていません．しかし彼らの体の圏と我々の体の圏の間には，正準な同型があります．2つの定義の間に数学的な違いはありません．

Lean は今の話でいう異星人流の慣例を使っています．異星人の $ι$ は Lean の field.inv に相当します．そして体での割り算は，Lean では field.div x y であり，これは field.mul (x, field.inv y) として定義されています．

オーケー，それで上手くいくことはわかった. でも何故まだ違和感を感じるんだろう？

それはおそらく次のような理由からでしょう．コンピュータの証明チェッカーがあなたのコードをチェックし, 特にゼロで割ったことがあるかどうかをチェックし，もし割ったことがあれば，証明が無効であるというエラーを投げるだろうと期待していませんか．Lean は上記の $y\not=0$ に対しては $f(x,y)=x/y$ であり，$y=0$ のとき $f(x,0)=0$ と定義された関数 $f$ を使っているだけであることを思い出す必要があります．特に, $(x,0)$ の形の入力に $f$ を適用することで誤ったことを証明することはできません．数学の割り算ではゼロで割ってから続けることで矛盾が得られますが，$f$ では得られません．例えば, 数学者が $a/a=1$ はすべての $a$ に対して真であると言っているとき，$a\not=0$ という暗黙の前提があり，これは表記から推測できます．real.div a a = 1 という Lean の定理は, $a\not=0$という仮定の下でのみ証明されるので, $a=0$ の場合は定理を使えません．言い換えれば，ゼロ除算の問題が現れる場所が変わるだけなのです．Lean は $0$ でこっそり割ることで $1=2$ を示そうとする証明を受け入れませんが，エラーはゼロで割るときではなく別のところで起きるでしょう．ゼロでないことを証明していない分母があるということが問題になるのは変わりません．問題は単に割り算をした時点で起こるのではなく，real.div に関して正しくない定理を呼び出した時点で起こるのです．

ツイッターでこの件を取り上げてくれた Jim Propp と Alex Kontorovich に感謝します．これで物事が明確になることを願っています．