Formalization of the Solution to the Hopf Problem

Oh wow, I'm fairly impressed. I wouldn't have expected AI to solve a problem this hard just now.

There have been claims of complex structures on s6 (or absence of them) quite a few times over the last 15 years. Some by acclaimed mathematicians. There was some discussions on HN a few days ago:

https://news.ycombinator.com/item?id=49412947

Surprisingly the (a, since multiple things have this name) Hopf conjecture was solved by human mathematicians around the same time. It’s the statement that S^2 x S^2 admits a positive sectional curvature Riemannian metric.

`solution.lean` is a 12mb file

I looks like we are breezing past the point where unassisted humans can understand any of this

I was thinking about trying this exact problem with AI. I missed that it had already been solved. It's not that surprising that someone else already tried it. What's surprising is that open problems get solved so quickly now that it's impossible to keep up with them all.

An exposition of the Alpöge-Claude construction, by a mathematician working in this area: https://philip-engel.github.io/S6.pdf