Formalization of the Solution to the Hopf Problem

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

`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.