A Claimed 100-Page Hopf Problem Proof Got Formalized Into 250,000 Lines of Lean Within Days

GitHub (plby/HopfProblem), via r/singularity·medium signalXBlueskyLinkedInCopy link

Levent Alpöge posted a claimed resolution of the 78-year-old Hopf problem, that the six-sphere admits a complex manifold structure compatible with its standard topology, written with Claude. Boris Alexeev's public HopfProblem repository holds the Lean formalization, with the statement adapted from the Formal Conjectures project. The r/singularity thread (229 upvotes) frames the days-long turnaround from claimed proof to machine-checked formalization as the actual story rather than the proof itself.