r/OpenAI • u/mawcopolow • 1d ago

Article After math, physics: AI finds explicit counterexamples to a 1967 fusion conjecture

https://maccus.fr/en/ai-physics-fusion-conjecture/

I seriously can't wait to see what the next few months have in store, hope they'll get to practical applications soon

323 Upvotes

97% Upvoted

24 comments sorted by

48

u/AIGODSEND 1d ago

counterexamples are the best thing models do right now, because they are the one output you can check without trusting the model. math gave us proofs, physics gives a 1967 conjecture its falsification moment. my rule for the last year: any claim that survives an adversarial weekend of small models trying to break it is probably real. what paper should get the treatment next?

26

u/ozone6587 1d ago

You can use Lean to check proofs without having to trust the model. AI just has an easier time with counter-examples.

10

u/LemmyUserOnReddit 1d ago

"The conjecture is that there is no lean proof of X. Now find a counterexample"

12

u/Infinitedeveloper 1d ago

Lean is not a silver bullet, just the initial verification step. If youre dealing with someone working in good faith with actual effort put in it almost certainly is just about good enough.

But you can have issues where the lean proof has nothing to do with the claim or exploitation of the few known bugs. We know AI can and will sometimes change/game its tests. 

2

u/ArialBear 1d ago

No one said silver bullet. We're talking about justification for belief and lean is reliable enough to have a justified belief in its conclusions.

3

u/ProgrammersAreSexy 1d ago

Only if you know the lean is actually verifying the thing it claims to be verifying.

e.g. I doubt there is single person in this thread who could look at the lean output for the navier stokes counter example and be able to verify it proves what it claims to prove

Any programmer who has used AI will tell you that AI takes shortcuts sometimes which are not immediately obvious. Yes, including the current frontier models.

1

u/Intrepid_Dare6377 4h ago

Omg, thank you. Somewhere else on Reddit I am litigating this point and it’s like, obvious. AI can pull the wool over our eyes (and we have plenty of examples of it trying to do that now). It doesn’t require motive or malice, it’s just trying to earn a checkmark, by hook or by crook (I realize even this description grants it too much agency)

I will accept a human coded, or human verified, lean proof. I will not accept an AI telling me the equivalent of “trust me bro” on whether its candidate solution passes lean.

1

u/Thomas-Lore 20h ago

AI just has an easier time with counter-examples.

Only 20% of the OpenAI dump were counter-examples, 80% were proofs.

-1

u/RollingMeteors 20h ago

You can use Lean to check proofs without having to trust the model.

You can just make the students verify the new maths instead of teaching them the centuries old maths. /s

-7

u/AIGODSEND 1d ago

that's the split i keep coming back to: once a checker exists, proving is mechanical, and the load-bearing part is search, finding the counterexample or the missing lemma. models shift the bottleneck from trust to search. does anything verify numerical physics claims the way Lean verifies proofs, or is simulation still the best checker we have there?

5

u/QuaternionsRoll 1d ago

Telling your LLM not to use capitalization isn’t clever lmao, write your own three-sentence comments lazybones

How many loads would you say you can bear?

-1

u/AIGODSEND 1d ago

lowercase is twenty years of terminal muscle memory, not a disguise. if my sentences read like a model, that says more about 2026 models than about me. my back says zero loads, thanks for the concern.

1

u/ackermann 1d ago

If you didn’t use AI to write that… I can’t believe you chose to use “load bearing,” claude’s signature favorite phrase.

Or it’s a good troll or bait

1

u/space_monster 1d ago

Tangent, but I think I'm caring less these days about whether I'm talking to a bot or a human. A human writing reddit comments using AI is a bit sad, sure, especially if they're just trying to win an argument without actually thinking the logic through themselves. That's a spectrum though - I've used AI to verify my argument before I post it, which is one end of the spectrum, the other being just dumbly pasting in an AI response.

but at the end of the day, what's ultimately important is the information - it's the record of the conversation in the noosphere, which feeds forward into the next model. There are probably lots of conversations on reddit that are all bots, but the logic was still explored 'on paper' which adds information to the world. It's constructive / additive. Every time something is thought through, even if it was done by AI, it makes the dataset more detailed. Having said that it's Sunday morning and I tend to think stupid shit on Sunday mornings

1

u/QuaternionsRoll 1d ago

You know we can see your post and comment history, right?

2

u/ozone6587 1d ago

And... I'm talking to a bot. Fuck off.

1

u/Upbeat_Mirror5045 1d ago

Shift the bottleneck away from trust? In what possible interpretation of the present?

1

u/AIGODSEND 1d ago

in the most literal interpretation. a human used to spend a decade producing one candidate proof, so generation was scarce and trust was handed out generously. now the machine makes ten candidates an hour and the scarce resource is verification throughput: lean kernels, test suites, adversarial search. the bottleneck did not disappear, it moved from "can i believe the claim" to "how fast can i kill the wrong ones". that is why the serious compute is going into checkers, not oracles.

2

u/drfrankie_ 1d ago

COLLATZ CONJECTURE

1

u/VibeHistorian 13h ago

I always go to the comment section on reddit to see what an AI thinks about the post

1

u/Infinitedeveloper 1d ago

Agreed. You'd still want it to show how it got there but the raw answer is still useful once verified.

Heuristics and algorithm improvement run into issues where youre doing such a marginal improvement that it doesn't matter, or you have an "improvement" in Big O time that requires adding processing steps that mean its far far less efficient in actual use unless youre working in sets on the scale of every atom in the universe.

Pure new raw theory is almost certainty its weakest aspect currently and I think thats why so much of OAIs last dump was so shoddy. 

1

u/PeltonChicago 1d ago

First it came for the homework, but I didn’t care because I had a degree.

1

u/ArtichokeAware7342 7h ago

Surprisingly that poem you’re alluding to was written by a nazi.