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.
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”?
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.
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.
The question is: are those real proofs, or just AI reasoning bugs again?
Holy shit. If an AI actually solves a Millennium Prize Problems we’re seriously entering superintelligence (but not AGI) territory.
In any case this should disprove the “AI is just a statistically typing monkey” theorem some AI skeptics are fond of.
The current examples of AI could never be described as a general intelligence let alone Superintelligence. These LLMs are definitely just a typing monkey (that was eloquently put).
They are literally generating text word by word with a next-word-prediction methodology.
With some tweaking they can be made to produce mostly coherent code and apparently also equations that balance. This does not make these algorithms geniuses. A calculator can also balance an equation, so that alone is not impressive.
The techniques LLM designers use to leverage statistical models in order to generate coherent sentences are actually rather impressive. It is legitimately quite a feat to make LLMs work as well as they do. But that does not mean that these outputs are anything like “thinking”, they’re just outputs. Data goes in, the machine churns, does some mystery math, and different data comes out.
These systems are not worth anthropomorphizing.
Depends how you define superintelligence, what I meant is a more specialized superintelligence than AGI. We already seen that with Go and Chess. But if AI overtakes humans in mathematics it takes on a different quality. But we will see. I doubt it stops here.
the machine churns, does some mystery math
Yeah, the sauce is in the mystery math. See my other reply. You’re making a category error.
