Formalization of the solution to the Hopf problem

The six-sphere admits a complex manifold structure compatible with its standard topology.

Based on A compact complex threefold fibred by tori over the projective line, and the six-sphere, originally shared on X by Levent Alpöge.

The repository includes a Comparator setup, with the statement adapted from the Formal Conjectures project.

lake update
lake exe cache get
lake build lean4export
lake exe comparator comparator/config.json

Type-check it online!