Formalization of the Solution to the Hopf Problem(github.com)
21 pointsby robinhouston5 days ago5 comments
  • nhatchera day ago
    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

  • VMGa day ago
    `solution.lean` is a 12mb file

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

    • glimshea day ago
      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.
      • VMGa day ago
        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

    • medlera day ago
      We pretty much crossed this bridge in 1976 with the proof of the four-color theorem: https://en.wikipedia.org/wiki/Four_Color_Theorem
      • elil17a day ago
        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)

        • tancopa day ago
          Is that really a problem? The only risk in a Lean proof is the LLM finding a bug in multiple kernels (2 with the standard setup) that would let it add a new theorem without legitimately proving it. If you have reasoning traces or send a second model to look at the proof you can easily detect that and file a bug report.

          For the rest you only need to check that the formal problem statement matches the actual problem and the proof is not using extra axioms. That's easy to check manually or with a simple script.

          • tux3a day ago
            Many mathematicians care about understanding the method and the tools used more than the result. LLMs have a large advantage in memory and reading speed, you can feed them the entire internet and published literature at training time, and then make them check dozens of papers in a few minutes at runtime. They might not be very creative, but they've seen that obscure 1990's theorem in the training data that happened to use an idea that might just work again.

            Reading the LLM's 12 MB lean output is a bit like trying to maintain a codebase that has been fully vibe-coded as a single giant file, by hand. Even if it's possible in principle, no one is going to enjoy that.

    • hyperpapea day ago
      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.
  • GPersona day ago
    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.
  • QuesnayJra day ago
    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.
    • GPersona day ago
      Unless you have access to the same compute limits as the guy at Anthropic, and the internal model they use, you probably would just have spent a lot of tokens without success. So you can take solace in that.
  • bamb008a day ago
    [dead]