As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.
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.
None of them did, though, despite how many tried. So empirically, it seems unreasonable to say human researchers can solve ‘problems like this’.
OpenAI the opposite.
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.
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.
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.
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".
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.
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".
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.
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.
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.
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.
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.)
I'd be furious.
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.
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?
Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.
I guess these little questions are what this article is really about.
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?".
Huh? We're about six decades past that moment.
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.
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
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.
But no, peer reviewed and published in a reputable journal is a fairly normal standard.
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.
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?
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.
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.
... spaz on the floor ...
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.
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
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.
A similar rule existed for the 100-year Wolfskehl prize established in 1906 for solving Fermat's last theorem; two years after publication.
Humans need to verify everything.
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.
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.
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
You mean the company that “accidentally” let their model perform a cyber-attack?
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.
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...
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)
Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.
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.
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.
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?
It's not. But Lean doesn't interrogate logical coherence, just internal consistency.
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.
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.
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.
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’
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.
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...
> 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.
> Which really makes me wonder about the actual value proposition of Lean then, but alas...
[1] there are sub-tools such as comparator that are designed for this type of use case. https://github.com/leanprover/comparator
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.
Do you believe no open questions remain as to the truth of the Collatz conjecture?
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.
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.
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.
It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.