Formalization of the Solution to the Hopf Problem
1–10 of 15 posts
Re: Formalization of the Solution to the Hopf Problem
#2I 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.
Re: Formalization of the Solution to the Hopf Problem
#3`solution.lean` is a 12mb file
I looks like we are breezing past the point where unassisted humans can understand any of this
Re: Formalization of the Solution to the Hopf Problem
#4An exposition of the Alpöge-Claude construction, by a mathematician working in this area:
https://philip-engel.github.io/S6.pdf
Re: Formalization of the Solution to the Hopf Problem
#5`solution.lean` is a 12mb file I looks like we are breezing past the point where unassisted humans can understand any of this
I understand the spirit of what you're saying, but "unassisted humans" isn't a good yardstick. There's hardly anything "unassisted" humans understand today... We require plenty of assistance from computer tools in most scientific discoveries.
Re: Formalization of the Solution to the Hopf Problem
#6Oh 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:
Re: Formalization of the Solution to the Hopf Problem
#7`solution.lean` is a 12mb file I looks like we are breezing past the point where unassisted humans can understand any of this
This is based on a 108 page prose paper that the repository links to. Of course, that's a very difficult paper as well, I don't know how many people would be qualified to read and digest it, but they do exist.
Re: Formalization of the Solution to the Hopf Problem
#8`solution.lean` is a 12mb file I looks like we are breezing past the point where unassisted humans can understand any of this
I understand the spirit of what you're saying, but "unassisted humans" isn't a good yardstick. There's hardly anything "unassisted" humans understand today... We require plenty of assistance from computer tools in most scientific discoveries.
fair, but we are approaching the point where it gets difficult to tell where the human still is involved
for all intents an purposes, the paper as well as the lean repo could be full LLM output with zero human involvement
Re: Formalization of the Solution to the Hopf Problem
#9`solution.lean` is a 12mb file I looks like we are breezing past the point where unassisted humans can understand any of this
We pretty much crossed this bridge in 1976 with the proof of the four-color theorem: https://en.wikipedia.org/wiki/Four_Color_Theorem
Re: Formalization of the Solution to the Hopf Problem
#10`solution.lean` is a 12mb file I looks like we are breezing past the point where unassisted humans can understand any of this
We pretty much crossed this bridge in 1976 with the proof of the four-color theorem: https://en.wikipedia.org/wiki/Four_Color_Theorem
The process of automating mathematics:
We understand the proof (most math from all of history) -> We understand how the proof was made (computer-assisted proofs like the four-color theorem) -> We have to trust the computer's explanation for how the proof was made (some LLM proofs)