科学・技術
ホップ問題解決策の形式化
Formalization of the Solution to the Hopf Problem (github.com)
要約
本記事は、6次元球面が標準的なトポロジーと両立する複素多様体構造を持つことを示し、ホップ問題の解決策を形式化したものです。Levent Alpöge氏がXで共有した論文に基づき、リポジトリにはFormal Conjecturesプロジェクトから改変されたステートメントを含むComparatorセットアップが含まれています。
全文翻訳
ホップ問題解決策の形式化
6次元球面は、その標準的なトポロジーと両立する複素多様体構造を持ちます。
これは、Levent Alpöge氏がXで共有した「A compact complex threefold fibred by tori over the projective line, and the six-sphere」に基づいています。
リポジトリには、Formal Conjecturesプロジェクトから改変されたステートメントを含むComparatorセットアップが含まれています。
lake update
lake exe cache get
lake build
lean4export
lake exe comparator
comparator/config.json
オンラインで型チェック！