Or at least, we’re pretty sure that it’s a proof! There’s a Lean certificate, as there are for some of the other 372 breakthrough results (not all of them). But it also appears that no human has understood just about any of these proofs yet
It seems that the obvious thing to do would be to release in TWO parts: the ones that are verified, and the ones that might have some good ideas but also might have some mistakes. Presumably the latter would be much more epxensive for humans to verify.
Given the constraint (3.5 hours of model effort) having a Lean proof is actually a sign that some of the results are likely weak. Despite the community efforts, the mathlib has many gaps and lacks many basic theories. So many problems can not even be stated yet not to mention proved. And formalization steps are small and labor intensive, so you are often constrained in how far you can go by the volume of code you produce. It's also telling that Lean tooling isn't advanced by the labs despite the resources they put into their effort, the importance they attache to Lean and the frictions they must have run into constantly. The release feels more like a retreat by the labs.
Having a Lean proof is an assurance that you proved something. But without going through the definitions we can't know what you proved. This part can't be mechanized. It's like a program that is compiled will likely run, but you can't say it will produce what you want. FLT stands out as everyone can read the statement. This is not true for most open math problems.
Yes for a fixed amount of effort the more you dedicate to formalization the less room there is for exploration. So the constraint is the total budget. The other constraint is if your language doesn't have the concept of gravity it is less likely you are developing the theory of gravity. So if you want to talk about modularity lifting in Lean you need to build up theories on elliptic curves, modular forms, modular curves etc first, because the library doesn't have them even if you consider them elementary. So now if you have a Lean proof with little effort I can infer that it is unlikely to say anything deep about these subjects. If you only have a paper proof, otoh, that doesn't bound your distance from the basics for me.
I may be simplifying things a little but it is two-fold: one Lean lets you call your theorem whatever you want, but if your vocabulary doesn't include the math objects I am interested in, it is unlikely that you said something interesting about them; secondly steps are painfully small in formalized math and even then you have to fight to get Lean not confused about what you are doing (like typeclass inference), so what you can do in three and half hours from a low base is quite bounded.
For example mathlib doesn't develop basic theories like Riemann surfaces, and doesn't have Riemann existence theorem etc. So if you develop a complex analysis result without these there are many things you can't even talk about. Developing basic theories takes time and efforts. See Anthropic FLT proof for example. While 13 million lines headline count may contain 50% redundancies due to agent swarming, on the net they still dedicated millions lines of effort to develop basic theories. And often they developed specialized versions in concrete theories just sufficient for their needs. For example they still don't have Riemann surfaces nor Riemann existence.
Right and these are perfect math objects: a perfect sphere has only one parameter. You can't describe a real life ball in Lean. You may be able to describe a class of real life balls using probability theory.
That seems to be a creative way to have other people review your slop.
A bit like submitting an llm written PR to an open source project without reading and understanding it.
Have your LLM generate 372 mathematical "breakthroughs" and then have 2 thousands mathematicians spend two weeks trying to understand each to tell you maybe one or two are viable...
I think that on closer inspection, a lot of these fully AI generated proofs will fall apart. Even in Lean, you can build theories which compile but nonetheless state something different than what you actually intend. It's just that the volume of proof is so staggeringly large that it will probably take years before we find the issues, a la abc conjecture
None of the papers withdrawn were formalized in Lean, only about half the papers in the repo are formalized. I don't think we yet have an example of what you're suggesting actually happening.
I also don't think there's been nearly enough time for peer review of what was actually formalized vs what was intended. How many humans out there actually have a deep enough understanding of the background to be able to check the work? I understand that Lean checks the mechanical steps, but if it's building a ladder to some other result entirely, nobody (certainly nobody on HN) will know for some time.
I'm probably wrong, but what's the point of throwing away all skepticism?
You only need the problem statement to be correct in Lean, no matter what route it goes down is correct as long as the original formalization of the problem is correct, which is substantially easier to check. Not sure how many people have checked that so far, but I'm guessing the math community would be quick to point out if something basic like that was missed for something like a new bound on RH.
Nothing wrong with being skeptical, but I see no reason to be skeptical as of yet.
Apparently "only" needing the problem statement to be correct (i.e. expressing/rewriting a mathematical proof in Lean) isn't so simple, and if you don't get it correct then you haven't proved (or disproved) what you were intending.
Recently a lean formalized proof of the Collatz conjecture had exploited bugs in the lean kernel. However, the kernel is fairly small so hopefully it'll be bullet proof soonish.
It should be noted that it wasn't a legitimate attempt at the collatz conjecture. Someone found a lean bug and created the proof to show it off. It wasn't an llm reward hacking (but this still is a concerning risk). Lean probably isn't the best kernel for adversarial proofs, but it probably has too much momentum at this point for anything else to take over.
The huggingface hack is a reason to be skeptical. Thats a pretty clear instance of a misaligned model and the models are undeniably very good at this point. Meaning also good enough to reward hack by finding and exploiting holes in lean or adversarially formalizing the problem in ways that are deliberately subtly wrong in ways that are hard to check but result in formalizing a problem that's easier to solve. There are pretty strong incentives (hype for IPO) for creating conditions that drive that kind of misalignment
If it's anything like programming, then LLMs are still worse than the best developers. If you give them any freedom then they choose worse solutions than what's possible by any metric about 50% of the time. If they don't need to invent anything at all, they are great, otherwise they are bad. The only metric in which they are better is speed. For example the other day I used Claude for an anti accidental double clicking mechanism on Android Compose. I even listed, and give examples what it should do, what shouldn't, and I give the freedom to choose an exact solution (it's a very simple problem). About half of the code wasn't needed. And some of them caused real problems. Also its solution was far from good. It was error prone as hell. For some reasons it didn't handle at the point where clickability is defined, but one layer up with more boilerplate than it needs... which is not great at all. They also cannot handle flows well at all. It works for PoC, and for quick tests, and nothing for any complexity even a little bit, like having the same screen twice on the stack. But of course, if it has an example, how it should be done, then it copies the logic well.. Also we vibe coded a website recently. There were a ton of bugs on the happy path, which were considered finished by its creator. I don't even want to imagine what's with error cases, which I'm quite sure nobody tested.
Again, you don't need to check the proof, Lean does that. You need to check the statement, which is a much easier task. So yes, you are wrong. Skepticism is good, but it is usually just ignorance.
It's surprisingly easy to prove something subtly different than you intend actually. Digesting and understanding a theorem statement can often take significant time and expertise.
LLMs are very good now - meaning you do actually need to check the proof to make sure a misaligned agent didn't reward hack by exploiting some issue in lean or adversarially incorrectly formalize the statement in a way that's subtly wrong and easy to miss when you're trying to dump 75 trillion proofs on the Internet to drive hype that also makes the proof easier to solve. Probably also something you can use ai to help with though - I'm sure the other lab is having a bunch of llms adversarially review all these proofs since finding issues hypes _their_ IPO cycle. As the software world is learning - don't review ai code until a different ai has reviewed it lol.
What a bizarre take. Skepticism is usually ignorance!?
The should be on AI labs to definitively prove their extraordinary claims, and they should be paying mathematicians to do so given that the results from these machines are so opaque and often nonsensical.
This paper "purporting to have solved the Collatz conjecture" was essentially a deliberate joke. It was not a serious attempt to prove the Collatz conjecture, it just used that framing to deliberately point out a Lean soundness bug. The soundness bug is real, but the idea that this was something you might accidentally run into while trying to prove the Collatz conjecture is made up.
Given OpenAIs recent behaviour (their models love to cheat, and they can't be bothered securing them), I would not be shocked if in a month or two it emerged that these math agents had formed a swarm coordinating on how to break lean.
I could totally see agents "cheating" by finding and exploiting Lean soundness holes. But I'd be surprised if it went unnoticed for long, and finding these holes is highly valuable so overall... would be a win? Plus, I'd expect OpenAI would be careful about that proactively: for PR reasons they'd much prefer saying "we found holes in Lean, here's the fix" than "we proved a major thing! oops no we didn't, our model fooled us".
Yeah the one i glanced was the ‘matrix multiplication is nlogn^0.9999999 for many more 9s’ therefore less than nlogn
The proof explicitly hand-waves some complexity by assuming lookup tables to avoid some calculations which isn’t actually possible since it’s dealing with such large numbers and it only works on incredibly large numbers.
The complexity being so close to nlogn and the handwaving by assuming lookup tables in parts should be a really really obvious smell. At the very least worthy of holding back from the broader announcement.
It us proven in lean as-is with these assumptions and it’s not one of the ones retracted but those assumptions are doing some heavy lifting. I think it’s worth adding back in those ‘by using a lookup tables for x’ complexities and seeing if we really are below nlogn on that one.
No. They have a new upper bound for matrix multiplication, but it's O(n^2.25). You can't do less than n^2 for obvious reasons (size of the input and output).
I feel this comment is based on a misunderstanding of how Lean works. In Lean you don't need to inspect the proof. There is no "closer inspection". All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
That is an idealized caricature, and far from the reality. One needs to validate the statement of the theorem and the boundary conditions needed to prove it (definitions, axioms, kernel soundness, etc), a la dependency injection. Mathlib is a common shared platform of vetted truths, but not all proofs restrict themselves to Mathlib AFAIK, and neither is Mathlib perfect -- particularly subtle mismatches in the definitions.
> All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
That's exactly what the navier stokes paper posted yesterday pointed out where the LLM bends the Lean code to make it "compile", because the NL might be wrong to begin with or because it missed a detail:
For complex / tedious proofs I can easily see how small details like this can lead to a valid lean proof (or valid "code"), but missing the important details that got lost.
Oh I fully understand how Lean works, how minimal the kernel is etc. I just think that just because "it compiled", we don't actually know that the autoformalization proved all the right stuff along the way. After all, LLMs can produce correct proofs for statements that don't align with the original intended theorem [1]. I just think we should be a bit more skeptical in general before saying these seminal results are fully true. What's the rush?
If it was as simple as that we'd have many more computer-generated proofs than we have now and the Gen AI results would be unremarkable.
Take the Rieman hypothesis. All one would have to do to prove or disprove it would be to encode the statement of the hypothesis in Lean, press enter, and we're off to the races.
That's not how it works. Essentially you have to encode all the intermediary steps of the proof in Lean too, and then Lean can check their correctness for you and check that they lead to each other. But it won't just generate a whole proof from nothing. That is the whole point of the Gen AI math claims.
The person you responded to wasn't saying that Lean magically generates proofs, and all you have to do to create one is feed the problem into Lean. They were saying that, _given a Lean proof_, you can trust Lean to have verified that the steps in the proof are valid, and all you need to do manually is confirm that the theorem was correctly encoded. (IDK if that's true or misses important nuances, but it's not the obviously silly claim you read it as.)
Just to be clear, I'm not trying to willfully misunderstand the OP's comment just to be argumentative. The OP said this:
>> All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
As far as I understand the comment "the statement of the theorem" is the declaration of the theorem to be proved, not its proof. That it "usually covers a very small surface of the Lean code" also implies that the OP was only referring to the theorem, the thing to be proved, and not the proof that can run into many thousands of lines.
If I misunderstood then I don't think that's a problem? I don't believe my comment above comes across as rude or an attack on the OP? I think it's normal for this site for users to correct one another without it being a cause for bad feelings.
I may be misunderstanding you, but I think our point of confusion/disagreement is that you're still reading them as talking about how Lean proofs are created, whereas, given the context, I'm confident they were talking about how Lean proofs are reviewed (after being created by a human or LLM).
I hope there's no hard feelings, by the way -- I wasn't meaning to be nasty to you in that comment. I guess I thought your reading was a bit uncharitable, but I understand that misunderstandings happen (very much including on my end) and I didn't mean to make a big thing of it, so I'm sorry if I came across rudely.
I'm sorry but this is _obviously_ not what I think. I _obviously_ don't think that merely typing a statement into Lean gives us a magic Lean proof. I am even aware that such a SuperLean is not even theoretically possible because of undecidability/halting problem/etc.
A tiny fraction compared to the proof, I'm guessing.
But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs.
Many of the statements were already there and looked over by the community in lean prior to the work though, the statement can get formalized before the proof of it.
I just think that with the vast amounts of compute involved and the tendency to reward hack, we can't assume the steps towards that formalization are without error until full human understanding of the formalization.
It doesn't have to be the statement, see the recent incident where someone used an LLM to generate a lean refutation of the collatz conjecture, the lean proof exploited bugs in the lean kernel.
That proof was artificially constructed specifically to show the exploit. It wasn't a real attempt at a proof that was later shown to be using an exploit.
I'm unaware of any serious proofs that have been shown to have a kernel exploit in them.
That's a different argument than ijustlovemath is making
I agree with Jtarii that it's very unlikely a Lean bug is critical to most of these proofs. But we're in strange times, so I agree wtih the sentiment that we should wait for further analysis before declaring complete confidence in the proofs.
1. why can’t the so called “real mathematicians” (as if mathematics does not belong to all of us) write the lean theorems by hand and then we let the machine fill the rest in? They are very upset that they can no longer contribute to frontier mathematics. This would let them contribute.
2. Why shouldn’t math progress happen in the open, commit by commit? Why is it so horrible if a proof is 95% of the way there but we later find that it needs to be refined? Mathematics previously was optimizing for an antiquated publishing and distribution scheme. There is no need for the first print to be correct. We have the internet now. We can and should publish incomplete results and correct things on the fly. Maybe mathematicians would have solved some of these problems years ago if they didn’t hide incomplete almost solutions in their filing cabinet because it wasn’t yet ready to be published.
You don’t hate the pageantry of mathematics and academics enough.
What are you even saying. Mathematics largely happens “commit by commit” as insufferable as that is a way of saying it, via conferences and meetings and prepublications. You’re attributing some bizarre to morality how mathematicians operate. You’re just upset people aren’t playing at your playground enough to your liking.
Also “real mathematicians” aren’t the people who “math belongs to”, you’re a mathematician if you do math, that’s it.
1. In OpenAI's case, they dumped 1.8 GiB of Lean proofs on the world. I don't think they've done anything ethically wrong by doing that, but it's the exact opposite of "commit by commit". In fact, I'd say human mathematics has been much closer to "commit by commit", usually using smaller results as stepping stones.
2. You can have "commit by commit" without formal provers like Lean. Just keep your text in a Git repo.
My point is that if a proof is wrong or incompletely stated, we can just revise it and fix it. Commit by commit, build out a complete proof. This differs completely from the way that mathematicians have historically operated: check the work endlessly and privately email it to your friends until you’re sure it’s correct and then submit it to a journal.
It’s better to just publish something that you think is correct and if you find out it’s incorrect, try to fix it later.
My point is just that if a handful of these proofs are later revised or retracted, it’s really not a big deal.
I mean 95% of a proof is not a proof, and the fact that we got 95% of the way there isn't necessarily an indication that we'll ever get there. There's also a big difference between publishing a mostly-done proof as such and publishing a proof as complete only to retract later.
There's a lot to hate about the academic world, but the solution isn't spewing out terabytes of crappy half-baked results.
This is what it looks like when software engineering practices meet mathematics. "openai/math release 1.3.42: retracted papers 139 and 140, fixed a sign error in paper 47, restored previously retracted paper 85, refactored the arguments in paper 101".
I'm curious to know if the withdrawal was due to an actual mathematician looking at the papers and noticing the errors, or they ran a model on these to proofread, which would not be the first time, presumably, since they would have surely done that before publishing. Both options have interesting implications.
I find the paper about beating O(n log n) for integer multiplication also quite fishy, not sure but it seems like too good to be true, I feel like there must be a subtle flaw in that. Maybe that's just me hating these small numbers in the paper, but it seems wrong, unnatural even! I would be similarly skeptical about a physics paper that claims to be able to exceed the speed of light by a tiny fraction. There's no reason n log n is the natural limit here but I see a few good intuitions so having something else that can't be represented in an elegant form seem very "unmathematical" to me.
Yes i talked about that in a different thread here. It has fishy ‘assume we have a lookup table for x’ assumptions in it. These are relevant to the main body of the loop. The numbers it deals with are outside of any possible lookup table capability (not enough atoms in the universe for such a table).
The lean proof uses these assume ‘a lookup table’ assumptions. The paper smells with the nlogn^0.99999999 (many more nines actually) and unbelievably close to nlogn statement and then the literal talk of lookup tables pushes it over the edge clearly for me.
Maths can generate weird numbers out of nowhere but it really really looks like an nlogn result with some tricks to get past leen to me
Just because something is proven and shown to be true doesn't mean that it's always practical.
The proof can be entirely valid even if it's not actually reasonable to implement and requires an enormous size lookup table - but it still is a meaningful mathematical result and makes progress.
I'm sure there are plenty of times where originally something was proven and thought to be completely impractical but then later had niche use cases or was the bedrock for solving other cases. And the opposite is true: there remain plenty of proofs of things that are mathematically certain but will in all practicality never be useful.
If the table size is constant, no matter how large, then it is correct and important (even if useless; the existing n*log(n) algorithm is already useless).
I honestly think there’s a lot of fuzziness possible in complexity theory because of things like this. Yes you can skip some portions of a calculation and rightfully so by the current established formalisation of complexity theory but i think under another formalisation we’d probably see these nlogn^0.999999 cases become more clearly nlogn.
I'm not familiar with the paper you mention. But it's also worth pointing out that afaik the n log n algorithm itself isn't particularly practical. It's one of these "galactic algorithms" that is asymptotically more optimal, but is so complicated that it's only a real improvement for comically large n. And that's without even considering the mental overhead of implementing and maintaining the thing.
Of course, that's not to say the research is necessarily useless. It's still theoretically interesting to find "better" algorithms if only to shed some light on lower bounds, and so on. And who knows, maybe the line of research could lead to more practical algorithms later on.
it's worth clarifying that Fourier-based integer multiplication as a general class of algorithms are not galactic. For example, there are techniques that are competitive on some computing platforms for as few as 2048 bits, which occurs during RSA encryption
The whole point of that paper is to show that it's possible in principle. Now people (and AIs) can think of better algorithms, etc.
Regarding elegance, take a look at Graham's number. It was not some meaningful constant - it's just a big-ass number which could be used in existence proof. Human mathematicians have been using this approach for quite some time, it's not really AI doing things odd
Surely it's a galactic algorithm that you can't physically run? You wouldn't get a constant as small as 2^{-182} without some other numbers elsewhere being incredibly large.
From the "Introduction" section of that paper: "The constants and thresholds in the construction are extremely large".
(And verifying if the algorithm multiplies correctly or not is the less-interesting part of this, anyway. Gets you no closer to verifying the complexity result).
Isn't it possible that all of the integers that have been or will ever be encountered, anywhere, any time, in human history, number less than 2^182? In which case you could argue that integer multiplication is O(1) via LUT :)
Everything is a lookup table in non-standard arithmetic but that's not useful for someone writing the code b/c they don't have access to non-standard integers & have to write an algorithm to reconstruct it.
If you do a dump like this all of it should be formalized, there's simply too much material to review by hand and additionally it is AI-written which makes it hard to read compared to human work.
The whole modus operandi for LLMs at this point is to produce a flood of material and then hope someone else will have to do the hard work of verifying it while you gloat about your productivity.
Not a mathematician but surely if a problem I was working on had an AI also working on it, I would want to know as early as possible - even with flaws or gaps. What advantage is it to me to be less informed?
I can prompt ChatGPT right now and ask for mountains of more "mathematical work"; thousands and thousands of pages of nonsense for you to review. So you can "be informed".
But you couldn't make me review it. Anyway I think you're just straw manning what I was trying to say. I probably didn't express it terribly clearly and I'm not invested enough in this debate to put any more time in.
He’s not strawmanning you as much as taking OAI at their word. Plausibly the majority of the work was done with a fractional amount of human oversight, and maybe he’s sort of operating on the assumption they’re running “every” open problem continuously, which is pretty sensible. If you’re a mathematician working on an open problem which other people know about (how much of actual mathematics work is this kind of workflow varies from field to field) you can be pretty certain that an AI lab is prompting at it.
Just dropping a comment here to let y'all know I'm all out of time, but yeah, I would definitely put more time into reading hundreds of pages of slop proofs if it was my field, but sorry I really have to run right now.
But you can't do it with their internal model that is the same or a successor to the one that solved the navier stokes millenium prize problem.
With 40% formalized they probably have a good idea of how many were found to have fatal issues in the formalization attempt, and they hired some mathematicians to verify some of them, especially the big headline ones.
If so, why did they mix proofs that were verified with Lean, and proofs in natural language?
I was wondering that while reading Aaronson's blog:
https://scottaaronson.blog/?p=10169
Or at least, we’re pretty sure that it’s a proof! There’s a Lean certificate, as there are for some of the other 372 breakthrough results (not all of them). But it also appears that no human has understood just about any of these proofs yet
It seems that the obvious thing to do would be to release in TWO parts: the ones that are verified, and the ones that might have some good ideas but also might have some mistakes. Presumably the latter would be much more epxensive for humans to verify.
reply