Hopf問題の解決をLeanで形式化：6次元球面が複素多様体になる証明
Formalization of the Solution to the Hopf Problem
数学上の未解決問題だったHopf問題が、Levent Alpöge氏の論文に基づき解決され、その証明がLeanで形式化されました。このリポジトリは、6次元球面が標準的な位相と両立する複素多様体構造を持つことを、定理証明支援系Leanを用いて機械的に検証可能な形で提供します。DeepMindのFormal Conjecturesプロジェクトとの比較セットアップも含まれています。
6次元球面は、その標準的な位相と両立する複素多様体構造を許容する。
HNでの議論
13- nhatcher
おお、かなり感銘を受けた。AIがこんな難しい問題を今すぐ解くとは思わなかった。
この15年間で、S^6上の複素構造についての主張（またはその不在）が何度かあった。中には著名な数学者によるものもあった。
数日前にHNでいくつか議論があった：
- GPerson
驚くべきことに、（同名のものが複数あるので、そのうちの一つだが）ホップ予想はほぼ同時期に人間の数学者によって解決されていた。それは、S^2 x S^2が正の断面曲率を持つリーマン計量を許容するという主張だ。
- VMG
`solution.lean` は12MBのファイルだ。
人間が補助なしでこれを理解できる地点を、あっという間に通り過ぎているように見える。