The proposal is that multiple checkers are unlikely to all have the same bugs so the more kernels you can use to check the results the more likely it is that the proof/code is consistent & correct (modulo set theoretic assumptions necessary for the correctness of the kernel).
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.
This is my hypothesis too. I work with LLMs daily. I use frontier models all the time, and I work in a startup that trains its own special-purpose models. At no point in the course of my work do I see anything resembling superhuman intelligence. I see superhuman stupidity, ie. stupidity so extreme that it exceeds what any human is capable of by orders of magnitude. So where are the superhuman math results coming from? Simple: translation. I've already thought this for a long time, that math is an obsfucated field and that programming already makes it far simpler to understand. So you train a machine to throw tons of compute at translating English into math programming, and blow the field out of the water because it's effectively been deobfuscated. Math proofs had a sort of security by obscurity; they were not genuinely supremely difficult, but rather very few people worldwide worked on them and their work was heavily obscured, so the great deobfuscation machine comes along and trivialises that aspect and suddenly the facade crumbles. I think all of this could have been achieved a long time ago had humans done the deobfuscation, but there wasn't sufficient programming <--> maths cross-domain expertise or financial incentive to develop it.
yes, I couldn't agree more, if like to add that "the industry" drive programming and maths apart:
computer science, or "Informatik/informatique" how some Europeans call it, was a branch of mathematics, and "the industry" pushed _very_ hard to get it "practical", make colleges and universities produce programmers, not computer scientists.
so they removed all "challenging" maths requirements from the curriculum, and you can graduate with much less formal rigour, and certainly without being a matematician.
that's also how python replaced scheme as a first teaching language.
This is a good thing, it was just implemented the wrong way. Should have split the degree into separate engineering and theoretical tracks with different names (CS and CE/SE). Today we get weird hybrids where the same degree is math focused in one school and more practical in another.
There is space for both but in the real world we need more engineers who know how to build systems properly than theorists who are great at formal reasoning. It's like structural engineering and physics.
This is not at all what mathematitians are saying. They say LLMs obfuscate proofs even more. Saying that mathematitians obscure proofs is nonsense. Maths requieres a big effort from the brain to be deobfuscated as you say, and deobfuscating maths requires understanding, which takes even longer. Thats why textbooks dont exist just after a new proof appears, it takes some time to digest it and identify the key parts.
Maths is a language, and learning a language takes time. Its like if I say that japanese made an effort to obfuscate their language just because i cannot read it or read it as fast as english.
LLMs are autimating some part of maths which is formal manipulation. It happens that computers are much better than humans at formal manipulation. In the same way that computers are much better at mathematical computations. That is the huge change in the field. But any working mathematitian can tell you that formal manipulation is just part of the research job.
The powerfull thing about maths is that formal manipulation has allowed humans to go further "for free": you just need to understand the foundations, and the formal system allows you to compute new results for free without needing to reunderstand them.
Reading very charitably: you can say that at the moment a lot of the AI's advantages seem to come from: (a) having read approximately everything, and (b) being willing and able to try out lots and lots of approaches without tiring or getting bored. You don't need to have superhuman intelligence, yet, when superhuman persistence still yields so much low hanging fruit.
It's not unique. I for one agree. Mathematics is obfuscated because mathematicians prioritize compactness on the page over ease of understanding. This results in confusing notation (single-character variable names, implicit multiplication, implicit parentheses) and large numbers of omitted steps.
If I want to understand some mathematics, my first step is always translating it to code. Modern code (excluding array languages) no longer has a culture of minimizing character count, and omitting "obvious" steps is not possible. LLMs are based on an architecture (transformers) that was originally designed for natural language translation, so it doesn't surprise me that they're good at this.
The notation and omitted steps are to increase legibility. You are focused on things that the author is intentionally telling you are not important. One of the challenges with Lean is that it requires a lot more effort to write things in a way that communicates what you're actually trying to say.
And anyone who's tried to write or read Lean will also tell you that understanding a complicated mathematical proof doesn't necessarily get any easier when it's completely formalised.
Had the same problem with browser extension for a while. I made Explayn because of it: a browser extension that explains any highlighted word, sentence, or formula in place, so readers can understand content without leaving the page. https://chromewebstore.google.com/detail/enjakhegoldmloghmce... Figured it might save you some time.
While I think there is some truth to this I think the framing is very uncharitable. The obscurity in maths comes from layers upon layers of abstraction because this is a useful way for humans to work with these complex ideas. I think we see some of this with these proofs that have been translated to lean: some of the proofs are millions of lines of lean, imagine trying to wrap your head around a codebase that is millions of lines! And just for a single proof! These impenetrable abstractions that mathematicians have created are like a mental model for a massive code base.
> 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?
(Former grad student in math here who has spent whole weeks formalizing in Lean lemmas that would be considered by professional mathematicians writing a mathematics text / paper as obvious ("without loss of generality we can assume that....", "it should be clear that...")
Probably very few or none.
These systems (mostly) don't help you discover new mathematics. They are a tool for formalization.
It just turns out that combining them with LLMs is the secret sauce. LLMs have quite a bit of creativity but make a lot of mistakes. The Lean typechecker never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.
I am a math undergrad and I tried lean. It probably is because of habit and familiarity but I still find lean proofs harder to read than NL proofs. I wonder what if the math education switch entirely to a formal language (not necessarily Lean) will be?
Once upon a time this was all there was, so it naturally was proven to work as it was easier than dealing with boards full of dip switches that predated them.
Naturally eventually we got macro Assemblers, followed by other attempts until FORTRAN came to be.
I have hear people make this comparison many times, but it just does not hold up under scrutiny.
I think the confusion stems from people being exposed to set theory, believing that formalisation is akin to writing those horrible set encodings of everything. Which I would agree would be akin to writing assembly.
But Lean, Rocq and Agda are all based in type theory. Which means it is more like the highest level programming language you can imagine! You have all the powers of abstraction, but you still have to convince the type checker – i.e. no “trust me, bro” casting, or even questionable while loops (“I promise this loop finishes at some point”).
These abstractions along with meta programming techniques (“tactics”) means that you can write readable correct proofs, but it takes effort. Math is extremely deep, and getting formalised all the way to the research frontier in a given subfield is a serious undertaking.
I think a lot of people have never actually tried using a proof checker and are forming hot takes based their imagined assumptions about how they work.
For anyone reading this, here is a very small example proof that + is associative over Nats in Agda (written using 1lab style equational reasoning syntax):
+-associative : (x y z : Nat) → x + (y + z) ≡ (x + y) + z
+-associative zero y z = refl
+-associative (suc x) y z =
suc x + (y + z) ≡⟨ ap suc (+-associative x y z) ⟩
suc (x + y + z) ≡⟨⟩
(suc x + y) + z ∎
Proof checkers are literally pure functional programming languages with richer type systems allowing you to leverage the curry-howard correspondence to map between propositions and types.
And here is another short and simple example of some Agda code (Did you know you can open modules in a type signature‽):
-- An element has at most one two-sided inverse.
inverse-unique : ∀ (M : Monoid) (open Reasoning M)
(x y z : type M)
→ y ⋆ x ＝ unit M
→ x ⋆ z ＝ unit M
→ y ＝ z
inverse-unique M x y z leftInverse rightInverse =
begin
y ⟪ sym (unitᵣAt y) ⟫
y ⋆ unit M ⟪ mapᵣ (sym rightInverse) ⟫
y ⋆ (x ⋆ z) ⟪ sym (associativeAt y x z) ⟫
(y ⋆ x) ⋆ z ⟪ mapₗ leftInverse ⟫
unit M ⋆ z ⟪ unitₗAt z ⟫
z
∎
where open Reasoning M
Not sure if all the unicode characters will render on HN, but the things left of the ⟪ ⟫-brackets is exactly what a text book in mathematics will have. While the things inside the brackets are just a functional-programming way of saying out the argument which would be left for the reader to make in their head for why each step holds.
(If you know Agda, I dare you to look carefully at this example!)
Assembly doesn't give you any safety or guardrails. It is basically the opposite. I think it would be a better comparison with something that is a very strictly typed and type checked language.
"Mathematics is commonly explained and recorded in symbolic and concrete forms that are easy to communicate, rather than in conceptual forms that are easy to understand once communicated. Translation in the direction conceptual -> concrete and symbolic is much easier than translation in the reverse direction, and symbolic forms often replaces the conceptual forms of understanding."
Ask a model (dsv4.1 flash works great on this) to explain the proof to you so you can get an idea of the overall concept and structure first. Formalized math tends to encode math a certain way to make it easier for Lean, which doesn't have a visual cortex, but harder for people.
As a former math major (and developer) it bugged me that lean is optimized for WRITING proofs and not for READING proofs. I'm noodling around with a language that is optimized for reading proofs:
You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.
Not saying your niche doesn't have value, but you can get interesting ideas from there.
Re aside: Ok, but consider that maybe it is rude to ask people to read something you didn't write without warning. I'd add a disclaimer whenever I post about it, and on the very top of the readme. Better: have a readme for humans that you wrote, and leave the current document as a readme for machines.
I don't understand what you're saying. Writing lean doesn't make it easier to formulate a proof. These LLMs are writing natural language proofs then formalizing after the NL proof is done. If humans were theorizing and exploring open problems in lean for the last 15 years, we'd be moving much slower than we have been with natural language.
Yeah, it's so funny seeing all these people discover Lean as if it invented mechanizing mathematics. Even Coq wasn't the first (might have been the first with dependent types though).
I concur with one of the other replies: very few or none.
This is putting the cart before the horse: Progress in verification has been huge because of LLMs. Mathlib PRs spiked at the release of Opus 4.6, any of the big formalizations would not have been here without LLMs.
More surprising to me, OpenAI claims they're doing informal reasoning and only after do the formalization. This seems to match the way in which they release things. Of course they will have Lean in the training data, but I think this supports the mirror hypothesis: We'd have the same progress in mathematics if proof assistants didn't exist, it would just be a pain to verify correctness.
Fully agree on the potential for Lean as a generic programming language.
Why? I’ve worked a bit with proving systems in my studies, but it seems to me that it is very hard to turn precise mathematical statements into useful programs. Perhaps for the core logic, but GUIs or any other state with the outside world is going to be difficult it seems to me
> 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?
Absolutely none of them. I have some experience formalizing math by hand in the pre-LLM era. I never started with making the formal proof. It is way too difficult. I don't think I've ever heard of any mathematician starting with a formal proof vs writing a natural language proof. Starting with a formal proof vs a natural language proof is putting the cart before the horse.
Without a natural language proof, or at least an idea of how to write the natural language proof, it is very difficult to write a formal proof. It's flying blind. I can blindly apply tactics, but without some larger plan to guide my formal proof, it's near impossible to make progress on all but the most trivial proofs. I don't think it has ever happened that a major proof was formalized before its natural language proof was written.
I don't think people appreciate just how labor-intensive it previously was to write a formal proof. It takes easily 10-1000x as much time for a human to write a formal proof vs a natural language proof. Even just formalizing a single undergraduate math textbook for certain subjects by hand was considered a multi-year project for a professional mathematician to undertake.
It is no surprise that OpenAI releases natural language proofs before they release formal proofs. Presumably the same difficulty difference applies to LLMs as well.
OpenAI having NL proofs earlier than Lean ones would require trust in the proof without ability to check it automatically. Perhaps Lean proofs are published later because it is considered a less important implementation detail or because there is a cleanup step that takes time.
No it's already explicitly stated that translation to lean is a second step that happens after NL proof is done. That's why some of 400 paper dump is without lean proofs.
I wonder how are they sure the proof is correct before making a Lean translation. How is the work loop organised to force LLMs to reach a valid solution. I thought the ability to make it possible was the main advantage of using Lean.
This is a great question. I am not a mathematician but I've had similar questions about my own field (CS/Elec) as well.
I have always felt that a huge amount of brain power has to be expended in understanding the jargon and getting used to the machinery. Once we get past that, what people would think are highly challenging subjects become rather simple and logical. An analogy I like to use is old people struggling with simple tech tasks. I remember an uncle of mine who approached me to fix their laptop which wasn't connecting to the internet. Turns out the laptop had not been booted in a while and the public certs shipped with the machine had expired. Said person is a highly accomplished person in their field but was helpless when it came to this task. After I solved the issue, the uncle was eager to know what the problem was and I tried to ELI5 it but to no avail. It is possible I did a really bad job of explaining it but there was too much basic machinery to cover. Why is there a public and private key, what is symmetric/asymmetric, why do certs even expire etc. I couldn't even touch on the foundational math underpinning all of it so I left him in a confused daze.
To any SWE, all this is table stakes but for non-tech people it is way too much jargon. Today, I'm confident my uncle could prompt his way to a working understanding of PKI - heck maybe even some aspects of cryptography and prime number math that makes it work. This is where I see LLMs making a massive difference - they can crunch a massive amount of jargon and leave only the actual trick/idea for you to understand.
This is also what people like Szegedy and Tao have also said - LLMs will make math closer to what SWE is - a lot more people doing it in workmanlike fashion rather than a small community writing papers. At one point, dynamic programming was some research topic that Bellman worked on and now every 20 year old works on tens to hundreds of these problems in the hopes of cracking a job. But I'm sure the Math field will go through some turbulence and I wish them the best. There will always be a need for SMEs who deeply understand a subject and can come up with interesting problems.
> 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.
Lean isn't super special in that regard. If you know Haskell or OCaml you are already pretty far along in at least being able to read Lean, as it comes out of a similar-enough tradition.
> If you know Haskell or OCaml you are already pretty far along in at least being able to read Lean
But that's not really what you want, right? Speaking as a programmer, I'd think you would want a language where the prerequisite is "knowing a math proof", not "some mathey PL"
> every programmer should be able to read
You want "every math major should be able to read it", not "every programmer"
> But that's not really what you want, right? Speaking as a programmer, I'd think you would want a language where the prerequisite is "knowing a math proof", not "some mathey PL"
Well, I was merely replying to this:
> [...] lean seems like a new foundational language family that every programmer should be able to read, [...]
Hell no. Writing formal proofs has huge overhead. Lean is not a productivity tool; it's a reliability tool. It's like asking if airport security made boarding faster.
Mathematicians are also not upset about Lean. They're upset because they feel like they're becoming redundant. And that has everything to do with LLMs and not Lean.
They're upset because they're having to change. They aren't being made redundant, but they're being made redundant for the part of math they most enjoy and for which they've traditionally been most rewarded.
The OpenAI proofs were all in English, and discovered by reasoning in English. Only afterwards was a portion of them translated into Lean. This step was only done to convince the mathematicians that the proofs were correct.
I think you have it backwards-- formalization is tedious and seldom yields insight.
It's the kind of low yield completionist task that you just don't do without something equivalent to cheap slave labor.
AI makes formalization more accessible and makes it more important: The current superpower of LLM powered research is that the LLM is absolutely relentless, but the relentless is a liability without a source of truth to check against.
They created an implementation of a Lean kernel in Lean (con-leche) and verified it as consistent.
Since there can be bugs in its compiler and runtime, they translated the code into Rust (con-ron), and verified the resulting kernel with another Rust-based verification tool.
There is also an ongoing verification project of Lean4, which is written in Lean4 itself. (My mental model is Lean4 := Raku and Lean := Perl)
So we have two verified kernels now, and another is awaiting release.
“ 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.
> 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)
60 comments
[ 3.1 ms ] story [ 150 ms ] threadIn 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
computer science, or "Informatik/informatique" how some Europeans call it, was a branch of mathematics, and "the industry" pushed _very_ hard to get it "practical", make colleges and universities produce programmers, not computer scientists.
so they removed all "challenging" maths requirements from the curriculum, and you can graduate with much less formal rigour, and certainly without being a matematician.
that's also how python replaced scheme as a first teaching language.
Not so fast. There were plenty more horses in that race.
There is space for both but in the real world we need more engineers who know how to build systems properly than theorists who are great at formal reasoning. It's like structural engineering and physics.
Maths is a language, and learning a language takes time. Its like if I say that japanese made an effort to obfuscate their language just because i cannot read it or read it as fast as english.
LLMs are autimating some part of maths which is formal manipulation. It happens that computers are much better than humans at formal manipulation. In the same way that computers are much better at mathematical computations. That is the huge change in the field. But any working mathematitian can tell you that formal manipulation is just part of the research job.
The powerfull thing about maths is that formal manipulation has allowed humans to go further "for free": you just need to understand the foundations, and the formal system allows you to compute new results for free without needing to reunderstand them.
Reading very charitably: you can say that at the moment a lot of the AI's advantages seem to come from: (a) having read approximately everything, and (b) being willing and able to try out lots and lots of approaches without tiring or getting bored. You don't need to have superhuman intelligence, yet, when superhuman persistence still yields so much low hanging fruit.
If I want to understand some mathematics, my first step is always translating it to code. Modern code (excluding array languages) no longer has a culture of minimizing character count, and omitting "obvious" steps is not possible. LLMs are based on an architecture (transformers) that was originally designed for natural language translation, so it doesn't surprise me that they're good at this.
(Former grad student in math here who has spent whole weeks formalizing in Lean lemmas that would be considered by professional mathematicians writing a mathematics text / paper as obvious ("without loss of generality we can assume that....", "it should be clear that...")
Probably very few or none.
These systems (mostly) don't help you discover new mathematics. They are a tool for formalization.
It just turns out that combining them with LLMs is the secret sauce. LLMs have quite a bit of creativity but make a lot of mistakes. The Lean typechecker never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.
it might(?) work? but abstractions exist for a reason (mostly...)
Naturally eventually we got macro Assemblers, followed by other attempts until FORTRAN came to be.
I think the confusion stems from people being exposed to set theory, believing that formalisation is akin to writing those horrible set encodings of everything. Which I would agree would be akin to writing assembly.
But Lean, Rocq and Agda are all based in type theory. Which means it is more like the highest level programming language you can imagine! You have all the powers of abstraction, but you still have to convince the type checker – i.e. no “trust me, bro” casting, or even questionable while loops (“I promise this loop finishes at some point”).
These abstractions along with meta programming techniques (“tactics”) means that you can write readable correct proofs, but it takes effort. Math is extremely deep, and getting formalised all the way to the research frontier in a given subfield is a serious undertaking.
For anyone reading this, here is a very small example proof that + is associative over Nats in Agda (written using 1lab style equational reasoning syntax):
Proof checkers are literally pure functional programming languages with richer type systems allowing you to leverage the curry-howard correspondence to map between propositions and types.(If you know Agda, I dare you to look carefully at this example!)
https://mathoverflow.net/questions/43690/whats-a-mathematici...
https://github.com/ityonemo/2b4m
The tradeoff is that it's more verbose, but you don't have to even know the language to properly decode a proof.
as an exercise for the language, I'm playing around with formalizing an online algebra text:
https://github.com/ityonemo/2b4m/tree/main/aata
LMK what you think
You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.
Not saying your niche doesn't have value, but you can get interesting ideas from there.
Aside: To some degree, the claudisms are the point since the PL is written by Claude and intended to be consumed by claude
This is putting the cart before the horse: Progress in verification has been huge because of LLMs. Mathlib PRs spiked at the release of Opus 4.6, any of the big formalizations would not have been here without LLMs.
More surprising to me, OpenAI claims they're doing informal reasoning and only after do the formalization. This seems to match the way in which they release things. Of course they will have Lean in the training data, but I think this supports the mirror hypothesis: We'd have the same progress in mathematics if proof assistants didn't exist, it would just be a pain to verify correctness.
Fully agree on the potential for Lean as a generic programming language.
Extraordinary claim requires extraordinary evidence.
Why? I’ve worked a bit with proving systems in my studies, but it seems to me that it is very hard to turn precise mathematical statements into useful programs. Perhaps for the core logic, but GUIs or any other state with the outside world is going to be difficult it seems to me
Absolutely none of them. I have some experience formalizing math by hand in the pre-LLM era. I never started with making the formal proof. It is way too difficult. I don't think I've ever heard of any mathematician starting with a formal proof vs writing a natural language proof. Starting with a formal proof vs a natural language proof is putting the cart before the horse.
Without a natural language proof, or at least an idea of how to write the natural language proof, it is very difficult to write a formal proof. It's flying blind. I can blindly apply tactics, but without some larger plan to guide my formal proof, it's near impossible to make progress on all but the most trivial proofs. I don't think it has ever happened that a major proof was formalized before its natural language proof was written.
I don't think people appreciate just how labor-intensive it previously was to write a formal proof. It takes easily 10-1000x as much time for a human to write a formal proof vs a natural language proof. Even just formalizing a single undergraduate math textbook for certain subjects by hand was considered a multi-year project for a professional mathematician to undertake.
It is no surprise that OpenAI releases natural language proofs before they release formal proofs. Presumably the same difficulty difference applies to LLMs as well.
I have always felt that a huge amount of brain power has to be expended in understanding the jargon and getting used to the machinery. Once we get past that, what people would think are highly challenging subjects become rather simple and logical. An analogy I like to use is old people struggling with simple tech tasks. I remember an uncle of mine who approached me to fix their laptop which wasn't connecting to the internet. Turns out the laptop had not been booted in a while and the public certs shipped with the machine had expired. Said person is a highly accomplished person in their field but was helpless when it came to this task. After I solved the issue, the uncle was eager to know what the problem was and I tried to ELI5 it but to no avail. It is possible I did a really bad job of explaining it but there was too much basic machinery to cover. Why is there a public and private key, what is symmetric/asymmetric, why do certs even expire etc. I couldn't even touch on the foundational math underpinning all of it so I left him in a confused daze.
To any SWE, all this is table stakes but for non-tech people it is way too much jargon. Today, I'm confident my uncle could prompt his way to a working understanding of PKI - heck maybe even some aspects of cryptography and prime number math that makes it work. This is where I see LLMs making a massive difference - they can crunch a massive amount of jargon and leave only the actual trick/idea for you to understand.
This is also what people like Szegedy and Tao have also said - LLMs will make math closer to what SWE is - a lot more people doing it in workmanlike fashion rather than a small community writing papers. At one point, dynamic programming was some research topic that Bellman worked on and now every 20 year old works on tens to hundreds of these problems in the hopes of cracking a job. But I'm sure the Math field will go through some turbulence and I wish them the best. There will always be a need for SMEs who deeply understand a subject and can come up with interesting problems.
Lean isn't super special in that regard. If you know Haskell or OCaml you are already pretty far along in at least being able to read Lean, as it comes out of a similar-enough tradition.
But that's not really what you want, right? Speaking as a programmer, I'd think you would want a language where the prerequisite is "knowing a math proof", not "some mathey PL"
> every programmer should be able to read
You want "every math major should be able to read it", not "every programmer"
Well, I was merely replying to this:
> [...] lean seems like a new foundational language family that every programmer should be able to read, [...]
Mathematicians are also not upset about Lean. They're upset because they feel like they're becoming redundant. And that has everything to do with LLMs and not Lean.
While everything seems crazy right now, the building blocks have been coming together for a long time now.
Software "engineers" really just want to be button pushers and design overly complex Rube Goldberg machines.
Waiting for "i made this" posts for formalized code ...
It's the kind of low yield completionist task that you just don't do without something equivalent to cheap slave labor.
AI makes formalization more accessible and makes it more important: The current superpower of LLM powered research is that the LLM is absolutely relentless, but the relentless is a liability without a source of truth to check against.
Since there can be bugs in its compiler and runtime, they translated the code into Rust (con-ron), and verified the resulting kernel with another Rust-based verification tool.
There is also an ongoing verification project of Lean4, which is written in Lean4 itself. (My mental model is Lean4 := Raku and Lean := Perl)
So we have two verified kernels now, and another is awaiting release.
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)
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/...