this post was submitted on 02 Aug 2026

15 points (63.6% liked)

Technology

87450 readers

3620 users here now

This is a most excellent place for technology news and articles.

Our Rules

Follow the lemmy.world rules.
Only tech related news or articles.
Be excellent to each other!
Mod approved content bots can post up to 10 articles per day.
Threads asking for personal tech support may be deleted.
Politics threads may be removed.
No memes allowed as posts, OK to post as comments.
Only approved bots from the list below, this includes using AI responses and summaries. To ask if your bot can be added please contact a mod.
Check for duplicates before posting, duplicates may be removed
Accounts 7 days and younger will have their posts automatically removed.

Approved Bots

founded 3 years ago

MODERATORS

L3s@lemmy.world

enu@lemmy.world

technopagan@lemmy.world

L4s@lemmy.world

L3s@hackingne.ws

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 2 weeks ago by eicker@lemmy.world to c/technology@lemmy.world

21 comments fedilink hide all child comments

top 21 comments

sorted by: hot top controversial new old

[–] eicker@lemmy.world 19 points 2 weeks ago (1 children)

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.

[–] AlteredEgo@lemmy.ml 3 points 2 weeks ago (1 children)

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"?

[–] eicker@lemmy.world 12 points 2 weeks ago (1 children)

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.

[–] AlteredEgo@lemmy.ml 4 points 2 weeks ago* (last edited 2 weeks ago) (1 children)

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.

[–] eicker@lemmy.world 3 points 2 weeks ago* (last edited 2 weeks ago)

It would be surprising if they didn’t release Astra. And yes, we’re living in crazy times.

[–] frongt@lemmy.zip 16 points 2 weeks ago

Ok so? Do the proofs hold up or not?

[–] Treczoks@lemmy.world 8 points 2 weeks ago

The question is: are those real proofs, or just AI reasoning bugs again?

[–] jobbies@lemmy.zip 6 points 2 weeks ago (2 children)

In other words its all marketing bullshit.

[–] ImgurRefugee114@reddthat.com 24 points 2 weeks ago* (last edited 2 weeks ago) (1 children)

So youre suggesting they secretly have Einstein standing in the server rack, making loud fan noises with his mouth and just typing really fast?

Either the problems were solved or they weren't. If they were, then that's evidence enough; doesn't matter if they model isn't publicly available.

Having those sudden breakthroughs come from a person or even a large group of mathematicians, suddenly and all at once, would be more surprising than a well-harnessed LLM figuring it out.

With that said, I'm curious about peer review of the actual proofs. Just because Lean builds them doesn't mean they're materially valid. It could very well be that it's completely wrong and it just hallucinated well enough to fool OpenAI into publishing it, which would be a hilarious egg-on-face moment

[–] iconic_admin@lemmy.world 12 points 2 weeks ago

I agree with you. If it solved it, it solved it. The title is an odd phrasing.

[–] RumRunningDevil@lemmy.zip 1 points 2 weeks ago

A few of the erdos problems have been independently verified. It's legit.

[+] AlteredEgo@lemmy.ml -6 points 2 weeks ago (4 children)

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.

[–] ImgurRefugee114@reddthat.com 9 points 2 weeks ago* (last edited 2 weeks ago)

The Decoder reported on August 1 that Brown said the lab had not spent much on each problem and that there were "no Millennium Prize Problems (yet)".

Just to be clear.

But yeah, if that happens, it will certainly be a major milestone.

[–] MadameBisaster@lemmy.blahaj.zone 3 points 2 weeks ago (1 children)

Ok, not sure I understand "AI is just a statistically typing monkey"? As far as I know AI simplified is just predicting what is statistically the most likely next word or is that wrong? I mean sure the way it predicts is complicated and word vectors are fascinating etc but highly simplified its a statistically typing monkey?

[–] AlteredEgo@lemmy.ml 5 points 2 weeks ago* (last edited 2 weeks ago)

It's a "category error" like saying hydrodynamics are just quantum mechanics. It does not describe the complex emergent behavior and doesn't really tell you anything. Or it's like saying psychology is how the neurons and synapses connect with each and exchange signals and that is all - this would not explain the mental processes between a marmot and a human. So it's not an accurate simplified description, just a description of the basic building blocks.

Afaik nobody knows how LLMs actually think, we only know sort of how to train them. They are researching how LLMs think with an equivalent to MRI brain scanning: Vista do LLM-MRI Python module: a brain scanner for LLMs

[–] unpossum@sh.itjust.works 0 points 2 weeks ago (1 children)

Nothing can disprove that to that crowd, I’m afraid.

[–] FauxLiving@lemmy.world 3 points 2 weeks ago

They think the problem is AI, when it's actually capitalism and securities fraud.

It's much simpler to fixate on the technology than to have to understand complex things like economics and history.

[–] Cocodapuf@lemmy.world 0 points 2 weeks ago* (last edited 2 weeks ago) (1 children)

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.

[–] AlteredEgo@lemmy.ml 0 points 2 weeks ago (1 children)

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.

[–] Cyanova@lemmy.dbzer0.com 2 points 2 weeks ago* (last edited 2 weeks ago) (1 children)

My understanding was that any hitherto success of LLMs in mathematics was in its trying approaches and information from different fields where they weren't traditionally applied (within mathematics), they have surfaced potential links but haven't created anything in any real sense. Still, a potential legitimate use for them that I personally hadn't anticipated.

[–] AlteredEgo@lemmy.ml 1 points 2 weeks ago

I mean that math is so far beyond me I have no clue if or how the proofs would "create anything" or lead to anything useful. I'm sure they do, besides adding a little bit to our civilization's knowledge.

I do suspect that LLMs think very "broadly" with a very broad knowledge but can't really reason very deep without training for a special problem. So rapidly trying different approaches does sound like how they do it. So maybe it is a little bit similar to a typing monkey except that it apparently did these proofs with a relatively limited budget.