-
Xenaプロジェクトとフェルマーの最終定理
- Xenaプロジェクトは、数学をコンピュータ上で形式化することを目標としている。これは、AIによる数学革命が起きた場合に、コンピュータが現代数論のフロンティアを拡張する助けとなるようにするためである。
-
フェルマーの最終定理の形式化
- フェルマーの最終定理（FLT）をコンピュータ上で証明する作業を進めている。この過程で、R=T定理をコンピュータに教えることが主要な課題である。
- Wilesの元の証明の代わりに、現代の一般化され単純化された証明を形式化しようとしている。
-
結晶コホモロジーと分割冪構造
- 結晶コホモロジーは1960〜70年代に開発された理論であり、数学の形式化に重要な役割を果たす。
- 分割冪構造は、結晶コホモロジーをコンピュータに教えるために必要な概念である。
-
人間の数学文書化の問題
- 数学の文書化の不正確さが明らかになっている。専門家の間では知られている内容でも、文書化がきちんとなされていない場合が多い。
- 形式化作業は、このような問題の解決に役立つ可能性がある。
-
形式化の重要性
- 数学を形式化することは、機械が自ら数学的議論を行えるようにするための重要な段階である。
- 多くの数学者は形式化の必要性を感じていないが、これは人為的な誤りを減らすために不可欠である。
-
結論
- 最近の発表で、分割冪の形式化の問題が解決された。これは、プロジェクトが再び軌道に乗ったことを意味する。
1件のコメント
Hacker Newsの意見
大学院時代に高速なコードを書いてBirchとSwinnerton-Dyer予想の研究を手伝っていた経験を振り返る。セミナーで反例を見つけたいと言ったところ、専門家たちが怒った。数学の深さは理解していなかったが、好奇心を刺激された。
数学における形式主義の発展を喜ばしく感じる。プログラマーとして、数学をより身近なものにしてくれる。形式主義の不足に対する不安には、好奇心で向き合うべきだ。
数学者はしばしば細部を省略しがちだと述べる。厳密な証明を求めるなら専門家の助けが必要だ。現代数学は不安定な土台の上にある。
アンドリュー・ワイルズがFLTを証明した過程を振り返る。1990年代の証明のやり方が、すでに古いやり方のように感じられる。
現代数学では文書化が不十分であることを強調する。形式的なシステムを通じて誤りを減らす必要がある。機械に数学的な論証を教えることが重要だ。
UI/UXデザイナーと開発者の役割の違いを説明する。デザインと開発では異なる思考様式が求められる。
Leanのような定理証明支援系が、数学における重要な道具になることを期待している。
Leanのコードを眺めるのは興味深い。最終的な証明文がユニットテストの役割を果たす。
数十年にわたり使われてきた数学的概念が、実は誤っていた可能性について疑問を呈する。
vitiatedという単語を紹介し、証明が誤っていたときに使うのに適していると述べる。数学者とエンジニアの間の隔たりに触れつつ、機械が数学を解くようになるにも性能向上が必要だろうと期待する。
数学文献の現状に失望を示す。1960年代から1990年代までの数論文献には問題があるだろうと予想する。専門家コミュニティが小さいほど、誤りは見過ごされやすい。