Lean now ships with verified kernels

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.

https://github.com/Verilean/sparkle

“ 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.

As someone who doesn't quite get all this, isn't the proposal here just checkers all the way down?

What does “verified” mean here? Someone has formalized verified the kernels or just different kernels cross check each others?