14
OpenAI Says Astra Solved 10 Open Math Problems With Lean Proofs: The proof files are public, but the new model is still private. (www.implicator.ai)
submitted 1 month ago by to c/technology@lemmy.world
23 comments fedilink hide all child comments
you are viewing a single comment's thread
view the rest of the comments
[–] 3 points 1 month ago (1 child)

I don't understand enough about math and lean proofs - do you mean it's possible nobody can interpret and explain how the proof goes in "human language"?

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 2 child comments
    •
  • [–] [S] 12 points 1 month ago (1 child)

    The impressive part isn’t that an AI produced a proof, it’s that Lean lets everyone verify it. The frustrating part is the model stays closed. Science advances fastest when others can reproduce both the result and the method, not just inspect the finished homework.

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 2 child comments
    •
  • [–] 4 points 1 month ago* (1 child)

    But they do plan to release the Astra model to the public "after it's finished" I assume?

    And yeah this Lean software sounds amazing, didn't know this was possible.

    I misread your last sentence in a way that create a different problem: Imagine AI starts producing more and more proofs at a pace that humans can't keep up with. So science advances, and humans can even make use of it, but can't verify or really understand the theory any more. Like we get better working machines, materials and processes, but do not understand why because we can't keep up. If that happened then that I guess would a significant stage in the singularity.

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 2 child comments
    •