フランスの研究所INRIAが開発しているCoqは証明支援システムの一種です。windows,macはインストーラーがあるようです。
https://coq.inria.fr/
大学院集中講義の機械学習講座の付録で「速習python教室」をやることにしたので準備を始めたのですが、「ラムダ式」を調べていたら、本来の目的からずれてこっちに来てしまいました。面白いですが、いまはCoqには深入りできないので、覚書のつもりで「今日の英語」の題材にしています。
さて、数学のいくつかの問題でコンピュータを用いないと証明できない（現状では）ものが知られていて、有名なものの一つは四色問題(四色定理、数百～数千個の配置が「還元可能」であることをしらみつぶしにすればよいことが証明され、その部分を計算機で1975年に証明)です。我々になじみがあるのがケプラー予想で、1998~2003年に膨大な場合分け（10万）と数値計算を使って「証明」されましたが、人間では4年かけても正しいかどうかが判定できず、論理に穴がないことを2014年に定理証明支援ツールで示して証明が確認されたことになっています。
https://ja.wikipedia.org/wiki/%E5%9B%9B%E8%89%B2%E5%AE%9A%E7%90%86
https://ja.wikipedia.org/wiki/%E3%82%B1%E3%83%97%E3%83%A9%E3%83%BC%E4%BA%88%E6%83%B3
上記wikipediaにも説明されていますが、ケプラー予想とは、球を3次元空間に詰めたときの最大充填率は面心立方格子と六方最密格子の値 π/3√2=74.0480489%である、というものです。予想は1606年、「証明」は2014年なので、400年以上かかっています。コンピュータと人間の知的融合で、まだまだ面白いことができるだろうと思います。
英語は https://en.wikipedia.org/wiki/Kepler_conjecture から
conjecture 「コ」ンジェクチャー （数学における）予想
astronomer アストロ「ノ」マー 天文学者
three-dimensional Euclidean space 3次元ユークリッド空間
“Imagine filling a large container with small equal-sized spheres: Say a porcelain gallon jug with identical marbles.”
小さい球で大きな入れ物を満たすことを考えよう。例えば同じビー玉を１ガロンの陶器の水差しに入れる。 （数学等、理論系の講義の説明はこういう命令形を使った言い方をします）
marble 大理石、ビー玉、分別、理性 level 4
Say 例えば
porcelain 「ポ」ースれイン 陶器
“Gauss proved that the Kepler conjecture is true if the spheres have to be arranged in a regular lattice.”
sphere スフィア 球
“But eliminating all possible irregular arrangements is very difficult. In fact, there are irregular arrangements that are denser than the cubic close packing arrangement over a small enough volume.”
eliminate 除外する
in fact 実際