>>761
どうも、スレ主です
情報ありがとう
ショルツェ氏のシステムで、IUTの正しさが立証されることを希望しています（＾＾

＜Google訳＞
https://www.nature.com/articles/d41586-021-01627-2
nature
ニュース
2021年6月18日
数学者は「大統一」理論におけるコンピューター支援証明を歓迎します
証明支援ソフトウェアは、研究の最先端で抽象的な概念を処理し、数学におけるソフトウェアのより大きな役割を明らかにします。
ダビデ・カステルヴェッキ

より良い理解
ショルツェの証明のリーンバージョンは、元のバージョンの100倍の数万行のコードで構成されている、とCommelin氏は言います。「リーンコードを見るだけでは、特に現在の方法で証明を理解するのに非常に苦労するでしょう。」しかし、研究者たちは、証明をコンピューターで機能させる努力が、それをよりよく理解するのにも役立ったと言っています。

Riehlは、証明アシスタントを実験した数学者の1人であり、彼女の学部のクラスのいくつかでそれらを教えています。彼女は、研究でそれらを体系的に使用していませんが、数学的な概念を構築し、それらについての定理を述べて証明する慣行についての彼女の考え方を変え始めていると言います。「以前は、2つの異なるものとして証明と構築を考えていましたが、今では同じものと考えています。」

多くの研究者は、数学者がすぐに機械に取って代わられる可能性は低いと述べています。証明アシスタントは数学の教科書を読むことができず、人間からの継続的な入力が必要であり、数学のステートメントが興味深いか深遠かを判断することはできません。それが正しいかどうかだけです、とバザードは言います。それでも、コンピューターは数学者が気づかなかった既知の事実の結果をすぐに指摘できるかもしれないと彼は付け加えた。

ショルツェは、証明アシスタントがどこまで行けるかに驚いたが、彼らが彼の研究で主要な役割を果たし続けるかどうか確信が持てないと述べた。「今のところ、数学者としての私の創造的な仕事に彼らがどのように役立つのか、私にはよくわかりません。」