12 ms·

Did an AI do that on its own though? I heard it was human mathematicians using a sophisticated machine as a tool.

• mstank 14d ago
  It sounds like LLMs were pretty useful to them…
  • ModernMech 14d ago
    So was Lean. Did Lean solve it?
    • zamadatix 14d ago
      Nothing is solved in isolation but credit usually goes to wherever the new work in the paper comes from instead of the whole mountain of previous mathematics or existing tools used. The most relevant of those get referenced and then this reference tree builds a tree of collective base work needed across history.
      • ModernMech 14d ago
        Usually credit goes to the people wielding the tools, not the tools themselves.
        • zamadatix 14d ago
          Usually there has never been a tool which performed the part relevant to getting any credit. E.g. in the first famous computer assisted proof (of the four color theorem) the computer only executed the resulting calculations defined from the new logic, it did not have part in the work needed to show those calculations could answer the problem nor did it come up with the actual calculations to do.
• meowface 14d ago
  All of the latest big proofs were driven by professional human mathematicians steering and priming the models, yes. All of the best AI-made software projects are also driven by experienced human software developers steering and priming the models. Does that mean the projects "aren't made by AI"? No, it just means AI is not quite good enough yet to fully replace humans, and, so, unsurprisingly, the best results will be obtained from people who are already great at a field and who take the time to squeeze as much force multiplication out of LLMs as possible. The AI is still doing well over 95% of the significant work.
  • TomGarden 14d ago
    While I agree with you, I think we also have to concede that this is not how these accomplishments have been presented. I'd argue most people I've seen talk about this online are unaware of the mathematicians steering the models.
  • basch 14d ago
    “Good enough to replace humans” isn’t necessarily the benchmark. The question is is a computer with a human stronger than a computer without a human. At what point does the hybrid go from being stronger, to the human getting in the way, or steering the computer in more wrong directions that right ones, or the human not being able to keep up. Does the human add enough extra randomness to be of value for a while, even as a minor co-processor.
    • TheOtherHobbes 14d ago
      Underappreciated point. The point of inflection is where humans switch from being a driver to a liability. But I don't think it's randomness, because that would be easy to add. It's more like a different perspective on the training data, a different set of perception categories, and a different set of skills used to work with all of the above. Those skills aren't very efficient, but they're the best we can do. We're used to their strengths but we don't like to think about their limitations. It's completely plausible that AI will replace some of them, and not implausible it could replace and improve on all of them.
• broast 14d ago
  The way frontier models work, that loop will get compressed to a one-shot within a version or two
• simianwords 14d ago
  > I heard it was human mathematicians using a sophisticated machine as a tool. where did you "hear" this? OpenAI said they only prompted it and it solved the problem in one shot without any help