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.
