OpenAI 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.
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.
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.
It would be surprising if they didn’t release Astra. And yes, we’re living in crazy times.