“Hales invests 20 person years in formalizing his Kepler conjecture result. And at the end, all he gets out of it is assurance that the thing is correct. Now, that is like, that's much less exciting than getting new math and new discoveries. … So in most cases, mathematicians know when things are right or not. They're not troubled by correctness.”
Machine Learning Street Talk · AI Research & Frontier Labs · October 2026
Context
Hartnett explaining why mathematicians resisted proof-checking software like Lean. He notes it can take around 20 lines of Lean for every line of informal math, and most mathematicians didn't see the payoff for what they care about most, discovering new math.
Transcript
…that. So he was not creating new math in the same way that like Andrew Wiles had to create new math when he saw Fermat's last theorem, where he had to like invent some very like powerful new concepts that just opened up entirely new branches of the field. So Hales' proof was not like that.
…I still like to think that the human understanding is still center in this. It may not be, but I think those are different quests at some point. It's like, can I make a machine proof stuff? Sure. But I'm interested in like understanding it. Right. And I'm still the one who has to understand it.
There is resistance because mathematicians don't see, by and large, or didn't see the value in that type of time investment. So Hales invests 20 person years in formalizing his Kepler conjecture result. And at the end, all he gets out of it is assurance that the thing is correct. Now, that is like, that's much less exciting than getting new math and new discoveries. It's especially not exciting in situations where you're already fairly confident that things are correct. So in most cases, mathematicians know when things are right or not. They're not troubled by correctness. There's a ratio called the De Bruyne ratio, which is the amount of lines of code you need to write in lean for every one line of informal math, like in a LaTeX PDF. And it's very high, 20 to 1, often higher. Mathematicians don't generally see the reason to invest that additional time just to verify the correctness of something. So that's really where the resistance comes from. They don't see the utility of lean for the thing they most care about, which is discovering new math.
This episode is supported by Cyberfund. If you're building at the frontier of AI, they want to hear from you. Cyberfund believes the future belongs to AI natives who want to achieve the impossible. And that's why they're introducing the monastery for AI native founders. It's an environment of pure…
Oh, Lean is both a programming language and a proof assistant. You can write codes. Lean is actually implemented in Lean itself. But the cool thing is that you can prove properties about your codes. You can state mathematical theorems. You can prove them. You can build a mathematical library like…
So in Kevin's book, Proof and the Code, he gives a precise definition of a kernel, which is a component in an interactive theorem prover like Lean. An interactive theorem prover has two basic components. A logical foundation, which determines how ideas are expressed and interact with each other…
More from Machine Learning Street Talk
