Xena のブログ記事 Division by zero in type thoery: a FAQ の翻訳を公開しました．
内容ですが，ゼロ除算の話です．数学ではゼロでの割り算が定義できないことは周知の事実ですし実際多くのプログラミング言語では 1/0 はエラーになります．
しかし lean では 1/0 = 0 になります．この直観に反する挙動についての解説記事です．
詳しいことは記事に書かれているので結論をざっくり書きます．
まず，おかしいことは何もありません．単に，便利だから 1/0 = 0 と約束しているだけです．
なぜ矛盾にならないかというと，a / b という演算の定義ではなく，a / a = 1 という定理の方に「分母がゼロでない」という制約条件をつけているからです．これは lean で形式的に数学を行う上での慣習です．
関数の方に仮定を持たせると，その関数を呼び出すごとに仮定をチェックしなければなりません．関数ではなくて定理の方に仮定を持たせる ことによって，この面倒を回避しているわけです．
私自身このルールが最初うまく呑み込めなかったのですが，この記事の英語版のおかげで理解できたという背景があり，役に立つと思ったので訳してみました．
