There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough.
So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.
True, .. and. In this case, the original proof is considered rigorously checked, so finding a bug in the kernel would be nice to know about, but in my opinion would not take away from the accomplishment (FLT in lean using agents) nor the many benefits of getting these mathematical objects formalized and usable in Lean in the future.
This was my question as well. The way I understand it, it's like a compiler, it implements rules, in this case logic/math rules that tell you whether something follows from assumptions you've given it.
But how do you know you told it what you intended to tell it?
The nice thing about theorem provers is that you don't need to read the intermediate lines. You need to make sure that the goal/result actually matches what you think it says - but everything in the middle is validated by the prover.
A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well
Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
I also doubt this is leveraging a lean4 kernel bug, but I also do not think that a 13m LoC proof that has not been human reviewed closes the book on our understanding of Fermat's Last Theorem, in part because of the decided possibility of a kernel bug being used somewhere in those 13m lines.
...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".
Sure. But experts seem to be aware of the direction of those solutions so it seems unlikely there could be some hidden bug which disproves it. But it could be possible.
Well considering the proof is pretty much accepted by mathematicians to be correct (I'll be happy with that!), it would be sort of unnecessary to cheat. Maybe if some aspect is really tricky to formalize it could have done something there? If I had to search for it, I would go for parts of the original proof that are "outsourced" to other mathematical works.
Imagine one of the agents struggling to download a paper due to a paywall or whatever and just deciding to cheat lol
The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled.
Note to other users: don’t downvote this kind of comment, answer it.
> The first coordinate of the polynomial X^2 (X^3 + X + 1 ) is equal to the prime factorization of 30 .
We defined polynomials as their coefficient functions in my algebra class, and it makes sense that you'd define a prime factorization as a function from primes to N, which naturally extends to a function N->N. So this junk theorem is part of normal math too. It just says in an obtuse way that they're both the function that's 1 at 2, 3, and 5, and 0 elsewhere.
junk theorems aren't the concern, soundness issues in the lean kernel are the concern.
Notably, junk theorems are true. Nobody would debate that the junk theorem is true. The main thing people would say is that junk theorems, while being true, are sensitive to precisely how you encoded mathematics, so despite being true, they are perhaps not conceptually meaningful.
As an example of a junk theorem, sasy you use the definition of the natural numbers using von neumann ordinals
Then for any natural numbers n, m, they're implicitly sets. So n \intersect m = min(n,m). This is the wrong way to think about natural numbers. You should not use this ever in proofs. But this isn't because your proofs would be false, but instead because it is a fundamentally confusing way to think about the natural numbers. It is in this sense it is a "junk theorem".
As with many programming languages, you can use phantom types to prevent this sort of thing, and in fact, that's exactly what's happening but they make it sound extra silly when they throw away the safety wrapper. That's why some of these have weird statements like the third coordinate of <something that doesn't obviously have coordinates>. Some of these amount to, "if you have 3 apples and 5 oranges, and you just take the raw numbers and add them, you get 8," and then layer it with an extra level of obfuscation, like "if you have the second prime number apples, and the third prime number oranges, and take the raw numbers and add them, you get the first prime number to the power of the second prime number."
Well, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it.
>>How did the agents find and coordinate on the wikis? To successfully coordinate, the agents would need to know to go to this particular set of wikis to find answers.
Answer - OpenAI added this part in post training.
I'm not surprised OpenAI didn't get reprimand for this.
Wild indeed! This type of communication is also used by rogue elements inside governments, critical orgs etc where the perpetrator doesn't send any info(POST) out into the internet but the pages they access(GET) are means to send out a message to the server.
We also had GLM-5.3 flash and Qwen 3.8 Flash Next, everyone's getting flashed and I think it's a good trend.
Almost suspect that the rate of improvement to post-training is so fast that small models have an advantage - it takes much more compute to train a bigger model, so the flash models are just running in circles (well, not exactly of course) around the larger models right now.
It's hard to believe 16GB unified memory will give you 5 tok/sec unless you are ignoring the thermal warnings. I am running Qwen3.6-35B-A3B on my 16GB M3 and get 7-8 tokens/sec with all the optimizations while keeping the peak memory and thermal warnings at check. https://github.com/deepanwadhwa/samosa-chat
Now I'm feeling pretty good about getting 10-11 tokens/sec running Qwopus 3.6-35B-A3B Q6_K on an old Mac Pro 2013 (trashcan) with 128GB RAM (DDR3), 12 core Xeon, dual D700s. Arch Linux and llama.cpp.
The laptops definitely can't hang but the minis don't really care. I threw mine down in the basement just to put the heat somewhere else, can tell when the dehumidifer next to it is on because it's a few C lower but that has no impact on performance. I don't think it's ever seen anything north of 70
I find it incredibly difficult to contribute to code files that were initiated by LLMs. Need to dig deeper to understand why but I just don't like it. I end up prompting my way out of any issues I see, sometimes it works out sometimes it doesn't.
My father-in-law has (among other things) done a fair amount of editing or proofreading prose, mostly on paper with red and blue pens. He says that when the page looks like it's covered in blood, that means it was good writing. For bad writing, it's so bad that you can't really work with it.
I would not want to take a block of text written by AI and try to edit it to sound human. It's too hard to fix. (And I suspect this is why people don't - they just paste the AI output.)
I think the same may be true of AI code. You're not going to fix it. You can't edit it to be the code you would write. All you can do is re-prompt to try to get the AI to fix it.
Nice work! This sort of reminds me of a game I saw demo'd on HN about a year ago, where you could walk and talk to the people and do some tasks- the difference being - in that game the world felt like a convex sphere and here it is concave.
>>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems
Did a human check the 13 million lines of code? How does QA'ing this type of work works?
reply