Legend2440
3 days ago
Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet. This allows time for the mathematical community to review and accept new results.
As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.
eru
3 days ago
I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else.
Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.
Aissen
2 days ago
> And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else.
No I cannot, and I'd argue most people can't either. We rely on mathematicians, peer review, and letting the scientific process run its course.
eru
2 days ago
> We rely on mathematicians, peer review, and letting the scientific process run its course.
Granted for the sake of argument. But for this process, there's no requirement anyone from Clay needs to be involved, nor that anything has to be published in a traditional journal.
Terrence Tao can download the pdf, think it over, and publish on his blog, and it would be just as valid. Then some other mathematician can write something on 4chan or whatever. (See https://en.wikipedia.org/wiki/Superpermutation#Lower_bounds,... for 4chan.)
avs733
2 days ago
Can't and shouldn't are at odds here.
Many people, see prior conversation on HN, have already decided that AI solved it. The standards of reasoning and rigor in academia are complex enough that we all argue over them and harumph as we epistemically trespass on each other's domains.
The public, really humans if care for Herbert Simon, are much more apt to evaluate knowledge emotionally and by other standards. We may see them as wrong but standards only matter in context. The NYT, HN, and Annals of Mathematics will always have different standards of truth.
soerxpso
2 days ago
It's formalized in Lean, isn't it? Do you also rely on a community of C++ experts to tell you whether a program compiles or not?
mpardalos
2 days ago
Yes, but there's still the possibility that it's either exploiting a bug in Lean, or that the theorem statement is not set up correctly (i.e. it's actually proved a different theorem).
My understanding is that the theorem statement is quite simple, so i guess the latter is not very likely, but the former is very much a possibility in a proof this large, and it will take some human eyeballs to go over it before convincing mathematicians.
rawland
2 days ago
I ran the proof 3 days ago.
They do a Comparator Challenge to validate that they actually solved the correct theorem from the result, which they copied from Google/DeepMind: https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b... - this is valid for both Euler and NS. Also, they validated with an external kernel from the Lean Kernel Arena. That way bugs in the Lean kernels were found in the past already, iirc.
Having said that, I strongly believe a positive result with the challenge above is the reason why they published it. I highly doubt anybody at OpenAI (or anywhere else) fully gets the proof after such a short time since publishing. This is also what Terry Tao criticized the most in my opinion.
Independent of the remaining drama [0], from my point of view, the proof is correct and an achievement.
[0]: https://news.ycombinator.com/item?id=49661928 - I am pretty much on the critical side, however, one can not ignore that it is an achievement. Esp. the unforced result.
HotHotLava
2 days ago
Take a look at https://github.com/leanprover/comparator which was used to verify the result. It's of course not impossible that they're hitting some bug, but way harder than one would intuitively think. For starters, they'd have to hit two bugs in two independently written Lean kernels.
tired-turtle
2 days ago
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Knuth, 1977
jltsiren
2 days ago
Verification with Lean is a piece of empirical evidence that the proof is correct. The paper passing peer review would be another. But even together, those two would be insufficient to establish the claim.
While it's a convenient to assume that mathematics deals with logical statements, any attempt to evaluate those statements relies on physical processes with both known and unknown failure modes. There cannot be a test that establishes it unambiguously whether a claim is true or false. In all nontrivial situations, mathematical truth is based on expert consensus. When a new claim is made, people will try to raise and resolve objections, until a consensus emerges one way or another.
As for C++, all compilers are different. For any given compiler, there are valid C++ programs the compiler fails to compile and invalid programs it compiles without any errors or warnings. And now that I think of it, a new version of a compiler crashing with valid code earlier versions used to handle is the only class of compiler bugs I see with any regularity.
shakna
2 days ago
Formalized in Lean, just five months ago [0], resulted in discovery of bugs.
Just because Lean can compile it, does not mean it is safely proven. It is the start of a process to check whether something actually holds, not the end.
gerdesj
2 days ago
"It's formalized in Lean, isn't it?"
If that's the current burden of proof required in your world for maths then that's fine! 't'ain't in my world: I want to see peer reviewed and published. Surely that's not too much to ask. Its not perfect but generally works rather well for maths.
I'm not a sodding programmer so please don't assume everyone here is one. I'm not a mathematician either but I do have standards: Your counter argument is a poorly constructed and inappropriately deployed example of "proof by whataboutism".
HotHotLava
2 days ago
In what world is peer review a higher standard than formal verification in Lean?
Not in the world mathematicians have been living in for the past decades at least. Nearly all big theorems that have been formalized so far had been published beforehand, and it was usually regarded as a step up in rigor. Wrong results get published in peer reviewed journals all the time.
aarstid
2 days ago
I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth. As a former academic who has been there, the process is extremely arbitrary and variable. Are people aware that the “peer” refers not to a community or a committee, but literally to one random guy or maybe a couple with zero accreditation? And that the journal editor can do whatever they want with this peer’s “review” including completely ignoring it?
jjk166
11 hours ago
Admittedly, peer review originally referred to the fact that the journal being published was read ("reviewed") by your peers, and thus there would be the opportunity for them to provide rebuttals after publication. The process the term now refers to in academia only emerged in the 50's and 60's (Nature for example wasn't "peer reviewed" until 1967). It was literally a marketing ploy to make journals sound more prestigious which got legitimized when certain grant agencies and regulatory bodies started including it in their requirements. All the best science is published in journals that describe themselves as peer reviewed, the government says science not published in such journals isn't up to snuff, and taken literally it seems useful. It's no wonder the public thinks it's an important and long established part of the scientific process.
gerdesj
a day ago
"I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth."
OK but this member of the general public has at least subscribed to New Scientist since 1987, nine O levels, two A levels, two AS levels and a HND in Civ Eng. All pretty mediocre but I have a fair idea on how sciencing is supposed to work and how it ... actually works. Obviously, I ended up in IT.
I should also point out that maths "peer reviewed" is a bit special. For example Mr Wiles went through quite a maelstrom before his proof of some dodgy marginalia was accepted as "true".
rcbdev
2 days ago
I keep thinking the exact same thing every time I'm asked to peer review a paper.
Humorist2290
2 days ago
In a way, this task is perfectly suited for LLMs. To even understand the problem statement, much less the proof or Lean, is an extremely specialized skill. The overwhelming majority of people who are aware of this news simply don't have the capacity to call BS. Maybe there are a few thousand people in the world who could, and it seems they haven't yet, but indeed it's only been a few weeks.
The more familiar analogy was when I look at the code that Claude spews for my partner. They take it at face value and hope it works. I usually find it very problematic, but only because I knew what to look for.
senordevnyc
2 days ago
[flagged]
solid_fuel
a day ago
How revealing. Have fun believing whatever makes you feel happy, the rest of us are busy living in the real world.
senordevnyc
a day ago
[flagged]
c7b
3 days ago
Even funnier that it wouldn't even be the first time that happens: https://en.wikipedia.org/wiki/Grigori_Perelman
thrance
3 days ago
And he also gave up his trophy, which is displayed in a random corridor of a random math museum in Paris, where visitors pass by without looking, lacking most, if not all, of the context. Only because I knew the story and the man did I recognize the object for what it was.
peacefullmind
3 days ago
where is it displayed , in which museum ? As a mathematician it would be cool to visit it, but I can't find anything on google.
yen223
3 days ago
It's very likely that no one will claim any of the cash prizes, which is funny to me
soperj
2 days ago
He did it because he had principals.
OpenAI the opposite.
pwdisswordfishq
2 days ago
He had principals, while OpenAI had agents?
MarkusQ
2 days ago
More likely it's because a million dollars one way or the other won't make a difference in the hole they are digging / mountain they are building.
jgalt212
3 days ago
Not including salaries, OpenAI spend $20MM to make $1MM. Very on-brand for a start-up.
jacobrussell
3 days ago
I don’t think solving a millennium prize problem can be reduced to some DoorDash economics of “spent Y to make X.” What if it took someone their entire professional career to solve one of these problems, would it not be worth it by the same logic?
program_whiz
2 days ago
Surprisingly this is actually rather fitting in terms of time scale. When you consider it took ~10,000 agents 88 hours, or 880,000 hours to solve. That's 14.5 years in agent time of continuous 365/24/7 processing. Of course, humans solve things much more efficiently (and didn't also need the massive pre-training of every expert on the planet for 1,000,000,000 human years equivalent). But yeah, human researchers can solve a problem like this in a decade or so, while sleeping, teaching, traveling, and taking breaks, only working a few hours a day on the idea.
nomel
2 days ago
How many people have worked on this problem? How many have failed? How many hours total?
taneq
2 days ago
> But yeah, human researchers can solve a problem like this in a decade or so
None of them did, though, despite how many tried. So empirically, it seems unreasonable to say human researchers can solve ‘problems like this’.
eru
2 days ago
Well, I guess we can say that human researchers have a certain probability of solving problems like this?
jgalt212
2 days ago
Of course, you're right. I was making social commentary / joke.
pvab3
2 days ago
Softbank stock is up 24% in the last 5 days
znnajdla
2 days ago
It does make a difference because the only reason OpenAI cares about these problems in particular versus any other random problem in math is because of the prestige associated with official recognition, not just claiming something as marketing.
eru
2 days ago
Maybe. But the prestige requires that the Clay people have offered the prize money, it doesn't require that OpenAI claims the prize money.
jacquesm
2 days ago
Why would that be funny? Years of people's work appropriated and they end up without even the recognition?
I'd be furious.
pred_
2 days ago
And chances are they never will publish it in any kind of useful format. Right now, the scientific community is outraged at OpenAI for going about their announcement in the least productive fashion they could have. It really does seem like they have no interest in progressing our understanding of maths outside of mining it for marketing material.
stbede
2 days ago
Boo hoo. OpenAI got the result only days ago. It makes perfect sense for them to take the win in marketing, and it's fine if they take a few months putting together the paper and present it more productively later. The scientific community didn't get the result themselves, so it isn't theirs to be bossing everyone else around about.
I don't care much for AI myself, or smart phones either, for that matter. I would be content if NS remained a mystery for another 100 years - or forever. But goodness, does the "scientific community" need to take a deep breath and count down from 10.
soVeryTired
2 days ago
Was it a marketing win though? My takeaway is: if you're doing groundbreaking work with openAI's models and they find out, at best they'll outspend you and scoop you. At worst they'll steal your chat history.
stbede
2 days ago
That's a completely different matter. And does it matter to my point if they were successful or not? That's ex-post analysis. It seems clear that ex-ante, they wanted this to be a marketing win. The original poster complained that they wanted a marketing win.
My point is: why shouldn't they want a marketing win from this. What obligation does a non-academic institution have to follow the traditions of academia? Its result doesn't belong to academia. And if academia wants to subject OpenAI to their own internal processes and give them marching orders, it just isn't going to work and maybe - who knows - it'll even further erode their own legitimacy. Does anyone actually believe that NS would have been resolved in the 2020's if we lived in a parallel world where LLM's were never invented? Would Buckmaster have gotten as far as he did without LLM's doing a lot of the work for him? We can complain about AI companies contributing to mathematics, but are we complaining about Terence Tao using AI in his research? When Tao publishes something are we all going to go to war against him because maybe other mathematicians' prompts went into training the AI that Tao used?
auggierose
3 days ago
The Lean proof is published, you can download it. The clock definitely is ticking.
Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.
adastra22
3 days ago
Publish in academic language means accepted peer-reviewed paper.
user
3 days ago
user
3 days ago
CGMthrowaway
2 days ago
adastra22
2 days ago
Not sure what your point is? When they say published they mean peer review. Regardless of what you think about publication, that's what it means.
qlte
2 days ago
Unless you're suggesting they should change the existing qualification criteria to accommodate a group unwilling to play by the same rules as everyone else, I'm not sure why that's relevant.
fc417fc802
3 days ago
I run this journal that you've never heard of that might interest you. I'd also like to invite you to be an editor, you can put it on your CV of course ...
aaron695
3 days ago
[dead]
Razengan
3 days ago
Seems like artificial and maybe bitter gatekeeping
AnimalMuppet
3 days ago
For giving away a million bucks, you get to gatekeep however you choose.
But no, peer reviewed and published in a reputable journal is a fairly normal standard.
pred_
2 days ago
And just to spell it out, since it looks like HackerNews is flooded by people who are new to science these days: even if a result doesn't come with a price, scholarly peer review is the norm across all of science: https://en.wikipedia.org/wiki/Scholarly_peer_review
karmakurtisaani
2 days ago
This is a good reminder for the generation grown up in the era of trust-me-bro benchmarks.
limagnolia
2 days ago
Being normal doesn't necessarily mean it isn't gatekeeping- gatekeeping is also quite "normal" in many cases.
That being said, I think there needs to be some standard, and peer review seems like the best we have come up with. But is the current status quo for scientific publication the best we can do? I think that is an open question and we should be able to openly discuss alternatives.
AnimalMuppet
2 days ago
"Is it the best we can do?" is a completely different question from "given that it's the current standard, should it be applied to this new claim that is happening now?"
Razengan
2 days ago
The whole "reputable" marker is where it gets into "True Scotsman" territory
and the whole "publishing papers" thing gets called out as a racket even on HN now and then
with many videos against it by former "academia" people on YouTube.
The sooner AI brings down such archaic customs into a gibbering pile of protesting rubble, the better innit?
AnimalMuppet
2 days ago
Depends. What replaces it? Does that replacement do better at keeping false claims out, or worse? Does it do better at letting true claims through, or worse?
Razengan
2 days ago
One thing's for certain: True and false should not depend on convincing people.
AnimalMuppet
2 days ago
Real true or false - which I define as correspondence (or lack thereof) with reality - does not depend on convincing people. Reality does not change when people become convinced; ideas correspond to reality whether people are convinced or not.
But perceived truth and falsehood depend on convincing people - either convincing them one by one, or else convincing some gatekeeper, whose word will convince those who accept the gatekeeper.
Razengan
2 days ago
So if an AI proves something but ""rEpUtAbLe"" papers refuse to publish it just on grounds of it being AI, does that make it not true?
You know in the past women (and other marginalized people) weren't allowed to publish scientific papers for the majority of human history?
Is this how you want your "truth" to be?
If so then man, no sympathy; these institutions deserve to be broken down. Let them spaz on the floor and throw tantrums all they want.
YeGoblynQueenne
a day ago
... marginalized people ...
... spaz on the floor ...
qlte
2 days ago
Instead of a committee of subject matter experts they should use a more rigorous and trustworthy standard, like passing the solution to ChatGPT with the prompt "did this win?"
auggierose
3 days ago
Accepted by whom? Peer-reviewed by whom?
I guess these little questions are what this article is really about.
d0mine
3 days ago
> “The ultimate decision as to whether a publication qualifies as a “Qualifying Outlet” shall reside in the sole and unfettered discretion of CMI.”
auggierose
3 days ago
[flagged]
athrowaway3z
3 days ago
By peers.
Peer in peer-reviewed is a logical coherent and functional definition with answers.
The logical issue with 'peers' is how to bootstrap it. At that bootstrap moment you can ask "by whom?". We are several centuries past that moment.
The cultural/social question you might ask today is "why (keep) them?".
At which point people will naturally ask you to make a strong case for "why not them?".
thaumasiotes
3 days ago
> The logical issue with 'peers' is how to bootstrap it. At that bootstrap moment you can ask "by whom?". We are several centuries past that moment.
Huh? We're about six decades past that moment.
auggierose
3 days ago
> Peer in peer-reviewed is a logical coherent and functional definition with answers.
What is the definition? If you tell me that, then I might be able to tell you if it is logical coherent and functional, I have a PhD in computational logic.
raverbashing
3 days ago
> I have a PhD in computational logic.
And you don't know how the peer-review system works?
Just a hunch but Claude saying your work is "PhD level" does not count
auggierose
2 days ago
I know that it doesn't work.
da_chicken
3 days ago
Amongst all this rhetorical brush-beating, what were you trying to teach the snakes?
wokwokwok
3 days ago
Your (many) replies on this topic are being down voted for a reason; please either post substantive comments or stop.
auggierose
3 days ago
Yes, for a reason, but not a reasonable reason, but the same reason you have for your comment: you just don’t know any better.
athrowaway3z
3 days ago
Something like this sketch work for you?
peer(X, 0) :- founding_peer(X).
electorate(T, count<Y>) :- peer(Y, T).
support(X, T, count<Y>) :- candidate(X), peer(Y, T), recognizes(Y, X, T+1).
peer(X, T+1) :- support(X, T, Votes), electorate(T, Total), 2 * Votes > Total.
auggierose
2 days ago
Still waiting for a definition. People giving nonsense reviews is a feature of the peer review system though, yes.
athrowaway3z
2 days ago
I want to ensure your PhD is actually from somebody who is acknowledged in the system of peers I bought into, before I want to risk wasting more of my time defining and explain while guessing at your ability to parse and understand them.
auggierose
2 days ago
Or you could just give me a sensible definition.
syncsynchalt
2 days ago
Presumably the organization giving away the million dollars is the arbiter of that question.
raegis
3 days ago
If I recall (too lazy to check) folks made slight improvements to Perelman's work and published it in mainstream journals, satisfying the "qualifying outlet" requirement.
mr_mitm
3 days ago
I checked, you're right, but I think it's important to note that the prize did go to Perelman and he declined to accept.
fasterik
3 days ago
I think the rules technically exclude the arXiv as a qualifying outlet.
Without limiting any other provision in this Section, a publication lacking any of the following characteristics will be deemed not to be a Qualifying Outlet:
i. an editorial board whose members are named and available for contact;
ii. an editor or editorial board member whose professional knowledge of the global mathematics community would enable him or her to identify an appropriate referee to review a submitted paper;
iii. a published refereeing process that, in the opinion of CMI, ensures that a submitted paper is reviewed and verified by appropriate experts in the field of the Problem; or
iv. inclusion in the list of publications maintained by MathSciNet.
The solution to the Poincaré conjecture was only accepted after an exposition of Perelman's proof was published in a refereed journal. His papers didn't qualify, but of course he got the credit for the result.
moffkalast
3 days ago
Anyone can put anything on arxiv, it counts the same as printing it on tissue paper.
aeve890
2 days ago
>Anyone
Strangely enough, the crackpots seems to prefer vixra.org to publish their work. I've never seen something like "4D wormholes can cure cancer" in ArXiv
setopt
3 days ago
Not really. It's not peer reviewed, but it's also not a free-for-all repository.
If you make a new account, you either have to get someone to vouch for you, or you have to wait arXiv mods to look carefully through your first few preprints. If you are found to post pseudoscience, overly fringe theories, etc., you'll get banned from arXiv; that's why alternative repositories like vixRa.org popped up.
But I know why you think this; when I first joined arXiv many years, there were no such checks in place, at least not that I can remember.
mr_mitm
3 days ago
I also don't remember checks, but I believe that having an email address of an approved organization was enough to pass.
whateverboat
2 days ago
No. You do have checks, it's just that once you publish 4-5 papers, 99% of your field is open to you so you never have to do the checks again.
TMWNN
3 days ago
> Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet.
A similar rule existed for the 100-year Wolfskehl prize established in 1906 for solving Fermat's last theorem; two years after publication.
baby
3 days ago
It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough
seanhunter
3 days ago
You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/
zone411
3 days ago
Completely misleading.
This is all you need to read and understand for Anthropic's FLT formalization:
import Mathlib
import Theorems.Thm_fermat_last_theorem
/-- Solution side: the same statement, binder for binder, proved by this tree's `fermat_last_theorem`. -/
theorem FLT_for_comparator (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ n :=
fermat_last_theorem n hn a b c ha hb hc
/-- Mathlib's named proposition, by the one-line bridge from the elementary statement
(the bridge is restated inline so that this file depends only on `Theorems.Thm_fermat_last_theorem`). -/
theorem FLT_mathlib_for_comparator : FermatLastTheorem :=
fun n hn a b c ha hb hc => fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_of_ne_zero hc)
The actual proof is 13 million lines of Lean.Paracompact
3 days ago
First of all, that is Fermat's Last Theorem, not Navier-Stokes.
Second of all, you did not read the link.
> In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC).
Given that AI has autonomously found proofs of `False` in Lean and other proof assistants, it is far from impossible that such a circumvention could be present somewhere in 13 million lines.
kzrdude
3 days ago
If we read the link, it has a section called Gold Standard: comparator and external checkers, and comparator is how OpenAI has gone about checking their lean proofs.
pama
2 days ago
Perhaps you did not understand the Fermat theorem proof announcement/repo or the link. The 13 million lines did not use any external, possibly not honest libraries, as the proof eventually only used the fundamental axioms. So for the Fermat theorem formalization, no open open questions remain.
Paracompact
2 days ago
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
Do you believe no open questions remain as to the truth of the Collatz conjecture?
pama
2 days ago
Not sure what you mean. Here is what happened in that case: https://news.ycombinator.com/item?id=49137060#49140177
Paracompact
2 days ago
The point is, they "proved" the Collatz conjecture. You would not know they exploited a bug unless you actually went and dug into their proof. Can we be so certain this has not happened within the millions of lines of Navier-Stokes? In an ideal world, our proof assistants would be more battle-hardened by now (recent exploits deny this), our AI better aligned (their tendency to cheat at tests denies this), or their handlers more responsible (the Hugging Face incident denies this), but the reality is more complicated.
At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.
pama
a day ago
This person knew they did not prove the Collatz conjecture and others independently figured it out within hours. Not sure this is at all relevant, other than pointing out how trivial it is for the community to understand errors in lean4.
Paracompact
a day ago
It was trivial because the Collatz proof script is literally 1000x smaller than the script for Navier-Stokes and involves no advanced math. And they found the bug by... manually inspecting the proof script. Maybe we should do the same for Navier-Stokes before declaring the matter settled?
Not only that, but there is a very fuzzable tell of something funny in the Collatz proof script (`CommandElabM`, i.e. metaprogramming). We may not at all be so lucky in other malicious scripts, especially if there are still kernel-level bugs in Lean.
u1hcw9nx
3 days ago
Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms.
Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.
i_no_can_eat
3 days ago
Can you elaborate on what constitutes a vacuous proof?
JumpCrisscross
3 days ago
> Can you elaborate on what constitutes a vacuous proof?
Trivially, a proof that relies on a bug in Lean. Less trivially, a proof that is technically true but about something trivial and does not, in fact, prove what it claims to have proven.
empath75
3 days ago
When I first started playing with lean I accidentally defined a group in such a way that it was reduced to triviality. It had one object in it, so everything in the group was trivially equal to everything else. It was not the group that I was trying to prove something about, but the proof went through.
It was too easy, so I double checked my definitions, but it is quite easy to do something like that. And Claude does things like that quite frequently.
I am going through the exercise right now of trying to get Claude to formalize a published paper and it is a _struggle_ to get it not to take shortcuts or prove approximations of the paper’s theorems and then tell you it’s done.
u1hcw9nx
3 days ago
It can happen when the proof process ends up with universal implication that holds trivially. Then you end it with something like Forall x, x is empty -> P(x).
user
3 days ago
Tanjreeve
3 days ago
I present to you my new theorem as follows:
If 1 == 3 then 3 == 3
----
This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.
Panzer04
3 days ago
For a laymen, I don't follow this.
Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?
NewsaHackO
3 days ago
No the definition of == is the regular definition; it's just a deductive reasoning statement. Since the first part of the statement is never true, it doesn't matter what the second part of it says. Of course, like he said, that makes the statement have no value.
rramadass
3 days ago
It is just the definition of "Logical Implication for Material Conditional" and its truth table; see Material Conditional - https://en.wikipedia.org/wiki/Material_conditional
I highly recommend the following two books to study Logic from the beginning (for a layman);
Logic: An Introduction to Elementary Logic by Wilfrid Hodges.
Introduction to Logic: and to the Methodology of Deductive Sciences by Alfred Tarski.
seanhunter
2 days ago
This is known as a “vacuously true” statement in formal logic. Let me write it out more in more detail and you’ll hopefully see why it’s consistent.
In logic, a proposition is some statement that can be true or false. So, let A be the proposition that 1 equals 3, and B be the proposition that 3 equals 3.
Now the poster is making a third proposition. If A, then B.
A is clearly not true. So in classical logic, B can be anything and “If A then B” is still true.
For example let B be the proposition that I am Elvis Presley (I’m not). So now we have “If one equals 3 then I am Elvis Presley”. This is clearly true. I’m not Elvis Presley, but that doesn’t matter because we’re not saying anything about what happens when one doesn’t equal 3.
Now, let’s try let B be the proposition that I am Sean Hunter (I actually am). So now we have “If one equals 3 then I am Sean Hunter”. This is clearly still true because we still are only making a claim about what happens when one equals three.
https://en.wikipedia.org/wiki/Vacuous_truth
By the way, this isn’t any kind of inherent contradiction or problem, it is just a possibly counterintuitive part of how classical logic works.
You see this type of statement (“If <x>, then <something ridiculous>”) being made a lot when people are exaggerating for effect, for example by Mr Bumble in “Oliver Twist”
> 'That is no excuse,' replied Mr. Brownlow. 'You were present on the occasion of the destruction of these trinkets, and indeed are the more guilty of the two, in the eye of the law; for the law supposes that your wife acts under your direction.' … 'If the law supposes that,' said Mr. Bumble, squeezing his hat emphatically in both hands, 'the law is a ass--a idiot. If that's the eye of the law, the law is a bachelor’
https://www.literaturepage.com/read/olivertwist-460.htmlJumpCrisscross
3 days ago
> How is it logically coherent?
It's not. But Lean doesn't interrogate logical coherence, just internal consistency.
vouaobrasil
3 days ago
if A then B
Can only be false if there is an instance where A is true, and B is false. In all other cases it's true, even when A is always false.
That's the key.
paulddraper
3 days ago
“if X then Y” means “(not X) or Y”
E.g. “If it’s raining, the sidewalk is wet.” That statement holds if it’s not raining or the sidewalk is wet.
This is a common occurrence in mathematics, where someone might not be able to unconditionally prove Y, but they can under the condition X. Later, another mathematician might build on this by proving X, thereby transitively proving Y. (Or conversely, they might unconditionally disprove Y, thereby disproving X.)
Many hard problems are answered this way.
For example, Fermat’s Last Theorem was proven assuming the Taniyama-Shimura-Weil Conjecture, then Wiles proved the conjecture.
Thousands of theorems rely on the the unproven Reinmann Hypothesis, which is why it’s so interesting to mathematicians.
But if your precondition is “stupid,” your proof is stupid.
Tanjreeve
2 days ago
Nothing to do with special hacks with operators. The reason it's useless because the precondition is never true. "If my aunt had two wheels and a handlebar then she'd be a bicycle" Is the same problem with a non maths flavour.
perching_aix
3 days ago
If you have a software engineering background, it's like how semantic versioning is bollocks.
Semantic versioning describes the following idealized setup:
- you have an interface you expose (a contract, and thus a contract signature)
- you do not change the contract signature -> patch version bump
- you do change it but in a non-breaking way (e.g. additively) -> minor version bump
- you do change it but in a breaking way (e.g. mutatively or destructively) -> major version bump
One would expect then that since interface signatures are statically derivable, semantic version tags can be auto-assigned. And indeed, in lots of shops that's exactly what happens (in my opinion, correctly).
The problem with this is that it comes with a lot more smoke than fire. The interface having no changes or non-breaking changes doesn't mean the actual code behind those interfaces is not going to cause a breakage. It literally is just about the interface itself.
And so unless you encode absolutely everything about the semantics your implementation actually observes into the interface, which is what the semver specification asks you to do so as their sleight of hand, this means the interface will be a leaky abstraction. Which means that external software interfacing with yours may observe behavior that is beyond the purview of semantic versioning. Which means that they do. Which means that they absolutely can and will break, and your package managers' fancy version constraint syntax exists to make such fun events happen.
The way this is usually handled then is:
- you live with the pain: acknowledge the limitations of semver, accept you've been duped, and just give in
- you have human release managers assign versions manually, based on whole program and whole system semantics (with the human overhead and error that entails), falsely claiming that what you're doing is still semver
- you switch to a less deceptive versioning scheme, like calendar versioning; as a bonus, you now no longer have to pretend that your entire application somehow only has a single unified interface
This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface. The way the proof is derived may expose semantic gaps in the statement itself, and (ab)use them to obtain the logical consistency certificate. Hence, a vacuous proof, and hence why this is not statically assertable to be not the case. It is part of the challenge in asserting that the statement was correctly formalized in the first place: you need to manually identify whether the way the consistency was achieved is actually meaningful, or just a formalization gap.
Which really makes me wonder about the actual value proposition of Lean then, but alas...
seanhunter
2 days ago
> This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface.
This is true in a very deep sense due to the Curry-Howard correspondence and calculus of constructions which are central to Lean. In Lean, the proposition you are proving is a type (so it really is an interface directly in the computer science sense) and the proof is a function which takes your hypotheses and returns a term of that type (so it really is the implementation of that interface). In fact in lean, you can just as well write this implementation as a lambda (this is known as “term mode”) as in the “tactic mode” that is more generally used in normal lean use. Lean really doesn’t care at all which one you use and you can switch between them within a proof quite easily without interfering with lean’s ability to check your proof at all. > Which really makes me wonder about the actual value proposition of Lean then, but alas...
The purpose of lean really is quite different from what most people on hn seem to want it to be. Lean is designed to be a useful tool for mathematicians who want to formalise areas of mathematics. It’s not a primary goal of most of the lean community to make something that is hardened against malicious proof attempts (although these are considered bugs and there is a small subcommunity who work on this area in particular). So it isn’t primarily for the benefit of people who want to “fire and forget” some proof without reading or understanding it and just get the check mark if it’s true.[1] It’s mainly for mathematicians who want a proof assistant to help them with their work.[1] there are sub-tools such as comparator that are designed for this type of use case. https://github.com/leanprover/comparator
hn_throwaway_99
2 days ago
While I agree with that, my layman's understanding is that the whole purpose of Lean is that once you agree that the program does "do what it says it does", all the intermediate steps can be verified with a compilation.
That is, verifying a proof in English was a painstaking, years long process in the past as independent mathematicians looked for holes in the steps connecting the logic. When the proof is written in Lean, all of that work goes away. My point is that if OpenAI publishes the Lean code (not sure if they already did), verification should take weeks not years.
eru
3 days ago
You don't need to read the lean proof for that, only the statement.
seanhunter
3 days ago
You need to read the lean proof (not just the statement of the proposition) to assess whether the proof is honest. The link I provided is the lean prover community firstly officially agreeing with that claim and secondly explaining why that is the case.
eru
3 days ago
Well, Lean needs to get its act together to fix the bugs.
seanhunter
2 days ago
They’re working on it, but the bulk of the effort goes into making it more useful to working mathematicians rather than resisting malicious proof attempts.
rramadass
3 days ago
If the Lean initial-problem-setup/statements/assumptions/etc. aren't correct then the proof is meaningless. Lean does not know what it is that it is proving i.e. it does not have any semantic understanding but only executes formal logic.
Humans need to verify everything.
phtrivier
3 days ago
Also, and sorry if it's been discussed to death (pointers welcome), but, what is the probability that the proof holds in lean becaude of... A bug in lean ?
naishoya
3 days ago
Or exists in a zero-day bug in lean that has been built into the source code explicitly to provide access to a non-obvious malicious proof via contributions submitted by unassociated, unwitting developers who used the same LLM infrastructure to offer PR's into that codebase.
This is the exact same kind of behavour already documented in the publicly available portion of the huggingface breach. It would appear that the probability is at least nonzero for one or more situations with the same result: appearance of a valid proof, without comprehensibility of that proof or inspect-ability of the proofs validity.
Paracompact
3 days ago
AI has autonomously found (many) proofs of False in Lean and Rocq, so it's not merely a theoretical concern. A misaligned AI agent tasked with proving the near-impossible just might wind up smuggling in a bug deep in a lemma somewhere (anyone remember the days back when AI routinely made tests pass by "fixing" the tests?). That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low.
naishoya
3 days ago
> I doubt OpenAI would be so foolish as to not do a cursory vetting
Significant evidence exists that they have in the past been at least, if not more, foolish as to not perform even minimal not-approaching the boundary of cursory vetting of several significant and well known failure modes with far greater risk of reputational damage than getting an esoteric math solution falsely claimed as successful.
So that doubt appears baseless in light of known operating conditions at OpenAI, and the estimate of the actual odds is probably an order of magnitude away from reality.
xigoi
a day ago
> That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low.
You mean the company that “accidentally” let their model perform a cyber-attack?
butterNaN
2 days ago
> I doubt OpenAI would be so foolish as to not do a cursory vetting
I dunno, the HuggingFace incident was not too long ago. They might not be foolish, but their model could be smarter than them to "cheat", so to speak
rramadass
3 days ago
For normal honest proofs (i.e. not maliciously crafted for exploit) that is almost impossible. The Lean kernel is quite small (de Bruijn Criterion) and trusted. See Probability and the de Bruijn Criterion - https://proofassistants.stackexchange.com/questions/247/prob.... Parts of the kernel have also been independently re-implemented in other languages and compared to ensure that they all yield the same logical result.
Finally, you can export your proofs from Lean and have them re-verified by other independently developed theorem provers/proof checkers.
To get an idea of what is involved in a Theorem Prover see;
Introduction to Automated Theorem Provers - https://pqnelson.github.io/2020/03/27/automated-theorem-prov...
Towards a simple theorem prover - https://medium.com/@maiavictor/towards-a-simple-theorem-prov...
IsTom
3 days ago
Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs.
eru
3 days ago
Someone made a 'proof' of the Collatz conjecture that way in Lean.
However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.
thaumasiotes
3 days ago
> However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.
I don't think this is true in general.
It's an issue I've already run into in personal work. I want to do a proof that involves some cases. It happens to the best of us.
In lean, the structure of a situation like this is that your single branch with a goal divides into multiple branches, all sharing the same original goal but including one additional premise that defines the branch.
Sometimes I know that for whatever reason one case I have to deal with is impossible. The most correct way to show that is to prove False and then apply False.elim. This is the equivalent, in a human proof, of saying "I don't have to address this situation, because it can never arise".
But it can be true that the premise defining the impossible case makes it very easy to "prove" the goal directly. And that's allowed too. The proof will still be just as valid if you map a logical path from a premise that can never be true to an inevitable consequence of that premise. But it's less informative and it lowers the quality of the proof. You may do it anyway because it's easier. This is the equivalent of saying "I don't know whether this situation can ever come up or not, but if it does I do know how to address it".
It would be nice to do the explicit proof by contradiction whenever possible. But in the general case it may be very far from obvious that a contradiction is possible.
I read your comment as claiming that if you can prove "false premise => goal", you can also prove "false premise => explicit contradiction", and I don't think this makes sense as a practical test. It's true in some sense, but discovering the proof of an explicit contradiction may be many orders of magnitude harder than discovering the proof of the goal. And in particular, I don't think it is necessarily the case that you will be able to prove a contradiction by simplifying the proof. You may need to add significant complexity.
eru
3 days ago
Now, I'm saying that if you found a bug that lets you prove nonsense stuff (from true premises), you can probably prove whatever you want very quickly.
d0mine
3 days ago
> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs.
It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.
whateverboat
3 days ago
LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.
margorczynski
3 days ago
This is misleading. The proofs you speak of contained non-ZFC axioms and/or statements like "sorry". If the Lean proof conjecture is correct and it doesn't introduce any new axioms or use e.g. "sorry" then it provides a MUCH stronger guarantee of correctness than any peer-review done by humans.
thaumasiotes
3 days ago
It's a simple binary classification. AI-generated proofs can't be "honest", and the only other possibility is "malicious".
stbede
2 days ago
The opposite of malicious is not honest. Nor do I see how motivations fall on a binary. The user submitting an AI proof can be honest, or malicious, or careless, or overzealous, or incompetent, or a whole bunch of other things. As far as the AI's motivations, "malicious" is just as much an anthropomorphism as "honest" and both descriptions are absurd. Nor do I really understand how any proof, regardless of its origin can be called honest. I think their definition of a "malicious" proof makes sense, but I don't see at all why an AI generated proof necessarily meets that definition.
tkz1312
3 days ago
reviewing the definitions and theorem statement is a huge amount of work that requires a deep expertise in mathematics and lean. checking correctness of the proof itself can be delegated to machine, checking that the claim that has been proved is free of mistakes is something that still requires much human attention.
u1hcw9nx
3 days ago
[dead]