Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- “ AI agents are very effective at finding vulnerabilities in our software.” No! AI can find code weaknesses not vulnerabilities. All vulnerabilities are weaknesses, but not all weaknesses are vulnerabilities.by runningmike
- > any remaining unsoundness bugs are most likely in Lean's compiler or runtime (including the bignum library). It is very unlikely that the same bug also exists in the Rust compiler or runtime, so by checking a proof with both con-leche and con-ron, you gain a high level of protection against this class of bugs
An awful lot of references for arbitrary precision arithmetic are just repackaging Knuth’s explanations, so I wonder if there could in fact be a bug in common (Although you would like to assume every other piece of software using them would have also hit any issues by now, so maybe it is fine)
by dwroberts - What does “verified” mean here? Someone has formalized verified the kernels or just different kernels cross check each others?by sinuhe69
- As someone who doesn't quite get all this, isn't the proposal here just checkers all the way down?by s_Hogg
- Sorry for almost completely unrelated shower thought but: there is an opportunity to name your blog “Leanardo”
- Lean plus AI is a winning combo: Lean is super precise but "narrow", AI is broad but lacks precision.
Before AI it was super tedious to formally express your software models in Lean, with AI this is super easy. See formal verification of consensus core in Ultima Cluster: https://github.com/PeterKnego/ultima_cluster/blob/main/docs/...
by 5ersi - Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?
In other words, how much of the developments this year are directly attributable to LLMs using lean, versus lean just being a significantly more productive language for some subset of mathematics compared to English and LaTeX?
Given how much we’ve seen formalized this year it feels hard to believe that this couldn’t have happened earlier.
Follow up question: do you think mathematicians would be as upset about the rapid changes in their field if they were the result of a collective shared effort on github, authored entirely by humans who all share the credit, versus that same outcome but authored by a large language model?
In other words, are the mathematicians upset about large language models, or are they really just upset that formalization and massive collaboration have turned out to be highly effective and has negated the heroic angle that mathematicians previously enjoyed, thinking in a locked room by themselves?
Food for thought.
A coworker recently remarked that lean seems like a new foundational language family that every programmer should be able to read, on par with C and Python, and I think it’s pretty hard to disagree with that. Next generations of models are going to be RL’d on Lean more and more because it pays dividends in winning the math war against their competitors, and this will benefit users of lean not only for mathematics but also as a general programming language and as a vehicle for other DSLs. For example, I think Sparkle (a Lean based HDL) or something like it makes a lot of sense in 2026 and beyond.