posted in Technology
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/openai-astra-10-math-problems-lean-proofs/
Implicator.aiOpenAI Says Astra Solved 10 Math Problems With Lean ProofsOpenAI paired its Astra proof claims with Lean certificates and a public repository. That makes the results checkable, but it does not make the unreleased model or peer review disappear.Replying to @eicker@lemmy.world
We’re reaching a point where the interesting part isn’t just whether an AI found the proof: it’s whether anyone outside the company can reproduce the result. Publishing Lean proofs is great. Keeping the model closed means the process stays a black box.
Replying to @eicker@lemmy.world
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”?
Replying to @AlteredEgo@lemmy.ml
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.
Replying to @eicker@lemmy.world
But they do plan to release the Astra model to the public “after it’s finished” I assume?
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.
Replying to @AlteredEgo@lemmy.ml
It would be surprising if they didn’t release Astra. And yes, we’re living in crazy times.