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

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

Formalizing a new paper, even if it was building on previously already formalized theorems, could be months of work just by itself, even with the natural language proof in hand.

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.

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.

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 math into 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.

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.

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.

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.

I remember attending a talk about Lean well before LLMs or the current AI craze. They were trying to automate mathematics for a long time.

While everything seems crazy right now, the building blocks have been coming together for a long time now.

> A coworker recently remarked that lean seems like a new foundational language family that every programmer should be able to read

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

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.

I mean we had Coq for the longest time.

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.

Now that the clankers do the work, programmers are suddenly interested in Lean, which has been available since around 2014.

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