7 ms·

That's what's covered by the "assuming you have formalized the statement correctly" parenthetical. Given a formal statement of what you want, Lean can validate

That's what's covered by the "assuming you have formalized the statement correctly" parenthetical. Given a formal statement of what you want, Lean can validate that the steps in a (tedious) machine-readable purported proof are valid and imply the result from accepted axioms. This is not AI, but a tiny, well reviewed kernel that only accepts correct formal logic arguments. So, if you have a formal statement that you've verified to represent what you are interested in by some other means, Lean can tell you whether the proof created by genAI is correct. Basically, there is a nigh infallible checker that won't accept incorrect hallucinations.

mjevans 8mo ago
I think the question is, how can humans have verification that the problem statement was correctly encoded into that Lean specification?
- mrtesthah 8mo ago
  They probably need to be able to read and understand the lean language.
  - aidenn0 8mo ago
    I can read and understand e.g. Python, but I have seen subtle bugs that were hard to spot in code generated by AI. At least the last time I tried coding agents (mid 2025), it was often easier to write the code myself then play "spot the bug" with whatever was generated. I don't know anything about Lean, so I was wondering if there were similar pitfalls here.
    - mkehrt 8mo ago
      In this case the human written statement of the theorem is small. Can there be bugs? Absolutely! But it's essentially a few lines of code worth of thinking. The lean proof checker then checks to make sure the proof actually proves the statement. In this case an AI is generating the proof, but if it "compiles" it's correct. The only thing humans need to check is the statement to be proven. (I don't know anything about this project but I've played around with lean and used other proof checkers more sesrisously).
      - rhdunn 8mo ago
        This is also an issue with non-AI and non-Lean proofs. Andrew Wiles' initial Fermat's Last Theorem proof initially had an error in it. That was spotted by peer review, fixed, and an updated proof was submitted.
    - saghm 8mo ago
      I don't disagree with you, but on the other hand, I feel the same way about code written by other humans, and that's not because they're necessarily worse at writing code than me, but because for code I've written myself, I've already spent time thinking about it, so I don't have to start from scratch when re-reading it. It's also not like I don't think I potentially write as many bugs as my coworkers either; it's just easier for me to catch my own up front as I'm coding than it is to catch theirs in code review. The two main differences are that I can have a more meaningful conversation with my coworkers about their approach, what bugs they might think are worth looking out for, etc. compared to an LLM (which in my experience will claim completely incorrect things about the code it wrote far more often than any engineer I've worked with even junior ones; the humans I've worked with have uniformly been able to report how confident they are in what they've produced being what they were tasked with without insane exaggerations), and that an LLM can produce a much higher volume of plausible-enough looking code in a given unit of time than most humans I've worked with. It's not obvious to me that these would be particularly severe problems in generating proofs though; unless the proof is so large that it would be infeasible to read through it in a reasonable amount of time, I would expect mathematicians to be able to make up for the lower quality conversations with the "author" by devoting more time to reading and thinking, or having someone else also read through the proof and talking through it with them. If anything, it's possible that the timeline for writing up a paper about the results might be better for some mathematicians than the equivalent amount of time most engineers have to spend reviewing code before the pressure to get it merged and move on to the next thing. (I'm aware that there is certainly pressure to get things published in academia, but I don't have firsthand experience, so I've tried to be intentional in how I've worded this to clarify that I want to avoid any assumptions about what the norms would be, but given the relatively wide range of time pressure that engineers might experience across the industry as a whole, I'd expect that at least some mathematicians might have some flexibility to spend extra time reading through an LLM-written proof, especially if it might be time they'd otherwise have to spend trying to come up with the proof themselves).
    - Jaxan 8mo ago
      If you want to check the statement, you only have to read the type. The proof itself you don’t have to read at all
    - bryanrasmussen 8mo ago
      As I understand it Lean is not a general purpose programming language, it is a DSL focused on formal logic verification. Bugs in a DSL are generally easier to identify and fix. It seems one side of this argument desperately needs AI to have failed, and the other side is just saying that it probably worked but it is not as important as presented, that it is actually just a very cool working methodology going forward.
      - baq 8mo ago
        Lean 4 is a bit awkward, but workable as a general purpose programming language, it e.g. supports sockets (with a C module, but so does Python.)
- ndriscoll 8mo ago
  The problem statement is apparently > Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn? Which seems like it's the type of thing you give as a homework problem to state formally in an intro class.
  - ccppurcell 8mo ago
    Are you an expert? Not gatekeeping here but I have no intuition for what is easy or hard to formalise. A lot of very simply stated graph theoretical results are apparently extremely hard to formalise.
    - dooglius 8mo ago
      I think you may be confusing specification of the problem and the formalization of the proof.
    - deleted 8mo ago
      [deleted]
    - codeflo 8mo ago
      > apparently When someone takes the time to explain undergrad-level concepts in a comment, responding with "are you an expert?" is a level of skepticism that's bordering on hostile. The person you're responding to is correct, it's rare that the theorem statement itself is particularly hard to formalize. Whatever you read likely refers to the difficulty of formalizing a proof.
      - IsTom 8mo ago
        > it's rare that the theorem statement itself is particularly hard to formalize That's very dependent on the problem area. For example there's a gap between high school explanation of central limit theorem and actual formalization of it. And when dealing with turing machines sometimes you'll say that something grows e.g. Omega(n), but what happens is that there's some subsequence of inputs for which it does. Generally for complexity theory plain-language explanations can be very vague, because of how insensitive the theory is to small changes and you need to operate on a higher level of abstraction to have a chance to explain a proof in reasonable time.
- johncolanduoni 8mo ago
  They can read the statement, and the definitions that the statement references. If everything it references is in a well-tread part of the Lean library, you can have pretty high confidence in a few minutes of going over the syntax.
- saghm 8mo ago
  Isn't that kind of a general problem with proofs, even when they're written by humans? There's nothing stopping someone from accidentally writing their own Lean proof that has slightly different semantics than an English version of the same proof, or even for their English proof to subtly miss something important or make an incorrect logical leap. This seems like a bit of a double standard, although maybe there's nuance here I'm missing.
  - teiferer 8mo ago
    One nuance you are missing is that the discussion is about formalizing the statement (the theorem), not the proof. The latter is what the article is about, but that doesn't suffice if you can't trust that the statement is also correctly formalized. These are the two main problems: 1. Formalizing a theorem. 2. Finding a formal proof. Part 2 is where AI could help as proof search is full of heuristics. That's also how humans find proofs and is one of the main skills of a mathematician. The formal proof can then be machine checked with well known and mature techniques not involving AI. Part 1 is the part that's missing and will always be hard. It's also the issue with formal verification of programs for which correctness criteria are often very complex and it's easy to mess up the formalization, so that even if you trust the proof, you can't trust that it proves the right thing.
- luckydata 8mo ago
  the same way you verify that any other program compiles? I don't understand the question tbh, it seems self evident.
  - NetMageSCW 8mo ago
    Compiling isn’t sufficient because it doesn’t tell you if the program matches the specification. A program that always says the temperature is 80 F will compile but is a terrible solution to what is the temperature outside at this location right now.
- deleted 8mo ago
  [deleted]
- digikata 8mo ago
  To borrow some definitions from Systems engineering for verification and validation, this question is one of validation. Verification is performed by Lean and spec syntax and logic enforcement. But Validation is a question of is if the Lean spec encodes a true representation of the problem statement (was the right thing specced). Validation at highest levels is probably an irreplaceable human activity. Also, on the verification side - there could also be a window of failure that Lean itself has a hidden bug in it too. And with automated systems that seek correctness, it is slightly elevated that some missed crack of a bug becomes exploited in the dev-check-dev loop run by the AI.
- threatofrain 8mo ago
  It’s far easier for Lean because the human has to read very little compared to generating whole programs.
f1shy 8mo ago
> This is not AI, A little bit nitpicking, but according to books like AIMA that is indeed AI. In the first chapter even any control system is classified as AI. Because of the reasons stated in the 1st chapter, I totally agree with the authors. The whole system is AI. That part is a verifier in a chain of “suggestions/instict -> verifier” like used in neurosymbolic systems for automated driving, for example.
rurban 8mo ago
Lean is doing logical AI, the classical AI part. Aristotle is doing the matching AI part, the modern LLM approach, previously called fuzzy logic. Both are AI.
- teiferer 8mo ago
  Calling Lean "AI" is quite a stretch. Though I'm also in the camp that dislikes the inflationary use of "AI" for LLMs, so I have sympathies for your viewpoint.
  - baq 8mo ago
    Finding a path in a maze was AI once.
    - chpatrick 8mo ago
      I think that definition is pretty obsolete for the last 20 years. To me "AI" is machine learning, statistical algorithms trained on data. That's not true for Lean.
      - baq 8mo ago
        So basically anything we don’t know how to write an algorithm for? I see where you’re coming from - but at the same time it’s actually an AI meme and smells of permanently moving goalposts.
heroprotagonist 8mo ago
Soo, it can definitively tell you that 42 is correct Answer to the Ultimate Question of Life, The Universe, and Everything. It just can't tell you if you're asking the right question.
- Someone 8mo ago
  No, it can tell you that 42 is the answer to (some lean statement), but not what question that lean statement encodes.
- davidwritesbugs 8mo ago
  I recently learnt that Douglas Adams wrote code and the ultimate answer was '*' - 42 in ascii
exe34 8mo ago
the argument here is that: 1. you write a proof in English that there is an infinite number of primes. 2. the llm writes 2+2=4 in lean. 3. lean confirms that this is correct and it's impossible that this proof is wrong.
- NetMageSCW 8mo ago
  You missed a whole section - a person creates a Lean formalization of #1 and Lean promptly says the AI proof is wrong because it doesn’t prove that formal problem statement. The question is in the person (or AI) creating the formal problem statement - how do you know it represents the problem the proof is supposed to be for? And the answer is for people in the field, in this case, formalizing the problem and verifying the formalization is easy. It is like generating an public key versus factoring it.
  - exe34 8mo ago
    I thought that's what I was trying to express between lines 1 and 2 above, but I may have failed to get it across. my understanding is that the danger is that the llm will create a proof that is correct but isn't about what the person thinks he's proving?
oh_my_goodness 8mo ago
>That's what's covered by the "assuming you have formalized the statement correctly" parenthetical. Sure. But it's fair to ask how to validate that assumption.
- fsmv 8mo ago
  Skilled humans must understand the problem and write the theorem statement.
bee_rider 8mo ago
How hard is it to go back to English, from Lean? Just as hard as going from English to Lean? If it is easier to convert backwards, maybe the AI can at least describe what the equations mean…

mjevans 8mo ago

I think the question is, how can humans have verification that the problem statement was correctly encoded into that Lean specification?

mrtesthah 8mo ago
They probably need to be able to read and understand the lean language.
- aidenn0 8mo ago
  I can read and understand e.g. Python, but I have seen subtle bugs that were hard to spot in code generated by AI. At least the last time I tried coding agents (mid 2025), it was often easier to write the code myself then play "spot the bug" with whatever was generated. I don't know anything about Lean, so I was wondering if there were similar pitfalls here.
  - mkehrt 8mo ago
    In this case the human written statement of the theorem is small. Can there be bugs? Absolutely! But it's essentially a few lines of code worth of thinking. The lean proof checker then checks to make sure the proof actually proves the statement. In this case an AI is generating the proof, but if it "compiles" it's correct. The only thing humans need to check is the statement to be proven. (I don't know anything about this project but I've played around with lean and used other proof checkers more sesrisously).
    - rhdunn 8mo ago
      This is also an issue with non-AI and non-Lean proofs. Andrew Wiles' initial Fermat's Last Theorem proof initially had an error in it. That was spotted by peer review, fixed, and an updated proof was submitted.
  - saghm 8mo ago
    I don't disagree with you, but on the other hand, I feel the same way about code written by other humans, and that's not because they're necessarily worse at writing code than me, but because for code I've written myself, I've already spent time thinking about it, so I don't have to start from scratch when re-reading it. It's also not like I don't think I potentially write as many bugs as my coworkers either; it's just easier for me to catch my own up front as I'm coding than it is to catch theirs in code review. The two main differences are that I can have a more meaningful conversation with my coworkers about their approach, what bugs they might think are worth looking out for, etc. compared to an LLM (which in my experience will claim completely incorrect things about the code it wrote far more often than any engineer I've worked with even junior ones; the humans I've worked with have uniformly been able to report how confident they are in what they've produced being what they were tasked with without insane exaggerations), and that an LLM can produce a much higher volume of plausible-enough looking code in a given unit of time than most humans I've worked with. It's not obvious to me that these would be particularly severe problems in generating proofs though; unless the proof is so large that it would be infeasible to read through it in a reasonable amount of time, I would expect mathematicians to be able to make up for the lower quality conversations with the "author" by devoting more time to reading and thinking, or having someone else also read through the proof and talking through it with them. If anything, it's possible that the timeline for writing up a paper about the results might be better for some mathematicians than the equivalent amount of time most engineers have to spend reviewing code before the pressure to get it merged and move on to the next thing. (I'm aware that there is certainly pressure to get things published in academia, but I don't have firsthand experience, so I've tried to be intentional in how I've worded this to clarify that I want to avoid any assumptions about what the norms would be, but given the relatively wide range of time pressure that engineers might experience across the industry as a whole, I'd expect that at least some mathematicians might have some flexibility to spend extra time reading through an LLM-written proof, especially if it might be time they'd otherwise have to spend trying to come up with the proof themselves).
  - Jaxan 8mo ago
    If you want to check the statement, you only have to read the type. The proof itself you don’t have to read at all
  - bryanrasmussen 8mo ago
    As I understand it Lean is not a general purpose programming language, it is a DSL focused on formal logic verification. Bugs in a DSL are generally easier to identify and fix. It seems one side of this argument desperately needs AI to have failed, and the other side is just saying that it probably worked but it is not as important as presented, that it is actually just a very cool working methodology going forward.
    - baq 8mo ago
      Lean 4 is a bit awkward, but workable as a general purpose programming language, it e.g. supports sockets (with a C module, but so does Python.)
ndriscoll 8mo ago
The problem statement is apparently > Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn? Which seems like it's the type of thing you give as a homework problem to state formally in an intro class.
- ccppurcell 8mo ago
  Are you an expert? Not gatekeeping here but I have no intuition for what is easy or hard to formalise. A lot of very simply stated graph theoretical results are apparently extremely hard to formalise.
  - dooglius 8mo ago
    I think you may be confusing specification of the problem and the formalization of the proof.
  - deleted 8mo ago
    [deleted]
  - codeflo 8mo ago
    > apparently When someone takes the time to explain undergrad-level concepts in a comment, responding with "are you an expert?" is a level of skepticism that's bordering on hostile. The person you're responding to is correct, it's rare that the theorem statement itself is particularly hard to formalize. Whatever you read likely refers to the difficulty of formalizing a proof.
    - IsTom 8mo ago
      > it's rare that the theorem statement itself is particularly hard to formalize That's very dependent on the problem area. For example there's a gap between high school explanation of central limit theorem and actual formalization of it. And when dealing with turing machines sometimes you'll say that something grows e.g. Omega(n), but what happens is that there's some subsequence of inputs for which it does. Generally for complexity theory plain-language explanations can be very vague, because of how insensitive the theory is to small changes and you need to operate on a higher level of abstraction to have a chance to explain a proof in reasonable time.
johncolanduoni 8mo ago
They can read the statement, and the definitions that the statement references. If everything it references is in a well-tread part of the Lean library, you can have pretty high confidence in a few minutes of going over the syntax.
saghm 8mo ago
Isn't that kind of a general problem with proofs, even when they're written by humans? There's nothing stopping someone from accidentally writing their own Lean proof that has slightly different semantics than an English version of the same proof, or even for their English proof to subtly miss something important or make an incorrect logical leap. This seems like a bit of a double standard, although maybe there's nuance here I'm missing.
- teiferer 8mo ago
  One nuance you are missing is that the discussion is about formalizing the statement (the theorem), not the proof. The latter is what the article is about, but that doesn't suffice if you can't trust that the statement is also correctly formalized. These are the two main problems: 1. Formalizing a theorem. 2. Finding a formal proof. Part 2 is where AI could help as proof search is full of heuristics. That's also how humans find proofs and is one of the main skills of a mathematician. The formal proof can then be machine checked with well known and mature techniques not involving AI. Part 1 is the part that's missing and will always be hard. It's also the issue with formal verification of programs for which correctness criteria are often very complex and it's easy to mess up the formalization, so that even if you trust the proof, you can't trust that it proves the right thing.
luckydata 8mo ago
the same way you verify that any other program compiles? I don't understand the question tbh, it seems self evident.
- NetMageSCW 8mo ago
  Compiling isn’t sufficient because it doesn’t tell you if the program matches the specification. A program that always says the temperature is 80 F will compile but is a terrible solution to what is the temperature outside at this location right now.
deleted 8mo ago
[deleted]
digikata 8mo ago
To borrow some definitions from Systems engineering for verification and validation, this question is one of validation. Verification is performed by Lean and spec syntax and logic enforcement. But Validation is a question of is if the Lean spec encodes a true representation of the problem statement (was the right thing specced). Validation at highest levels is probably an irreplaceable human activity. Also, on the verification side - there could also be a window of failure that Lean itself has a hidden bug in it too. And with automated systems that seek correctness, it is slightly elevated that some missed crack of a bug becomes exploited in the dev-check-dev loop run by the AI.
threatofrain 8mo ago
It’s far easier for Lean because the human has to read very little compared to generating whole programs.

f1shy 8mo ago

> This is not AI, A little bit nitpicking, but according to books like AIMA that is indeed AI. In the first chapter even any control system is classified as AI. Because of the reasons stated in the 1st chapter, I totally agree with the authors. The whole system is AI. That part is a verifier in a chain of “suggestions/instict -> verifier” like used in neurosymbolic systems for automated driving, for example.

rurban 8mo ago

Lean is doing logical AI, the classical AI part. Aristotle is doing the matching AI part, the modern LLM approach, previously called fuzzy logic. Both are AI.

teiferer 8mo ago
Calling Lean "AI" is quite a stretch. Though I'm also in the camp that dislikes the inflationary use of "AI" for LLMs, so I have sympathies for your viewpoint.
- baq 8mo ago
  Finding a path in a maze was AI once.
  - chpatrick 8mo ago
    I think that definition is pretty obsolete for the last 20 years. To me "AI" is machine learning, statistical algorithms trained on data. That's not true for Lean.
    - baq 8mo ago
      So basically anything we don’t know how to write an algorithm for? I see where you’re coming from - but at the same time it’s actually an AI meme and smells of permanently moving goalposts.

heroprotagonist 8mo ago

Soo, it can definitively tell you that 42 is correct Answer to the Ultimate Question of Life, The Universe, and Everything. It just can't tell you if you're asking the right question.

Someone 8mo ago
No, it can tell you that 42 is the answer to (some lean statement), but not what question that lean statement encodes.
davidwritesbugs 8mo ago
I recently learnt that Douglas Adams wrote code and the ultimate answer was '*' - 42 in ascii

exe34 8mo ago

the argument here is that: 1. you write a proof in English that there is an infinite number of primes. 2. the llm writes 2+2=4 in lean. 3. lean confirms that this is correct and it's impossible that this proof is wrong.

NetMageSCW 8mo ago
You missed a whole section - a person creates a Lean formalization of #1 and Lean promptly says the AI proof is wrong because it doesn’t prove that formal problem statement. The question is in the person (or AI) creating the formal problem statement - how do you know it represents the problem the proof is supposed to be for? And the answer is for people in the field, in this case, formalizing the problem and verifying the formalization is easy. It is like generating an public key versus factoring it.
- exe34 8mo ago
  I thought that's what I was trying to express between lines 1 and 2 above, but I may have failed to get it across. my understanding is that the danger is that the llm will create a proof that is correct but isn't about what the person thinks he's proving?

oh_my_goodness 8mo ago

>That's what's covered by the "assuming you have formalized the statement correctly" parenthetical. Sure. But it's fair to ask how to validate that assumption.

fsmv 8mo ago
Skilled humans must understand the problem and write the theorem statement.

bee_rider 8mo ago

How hard is it to go back to English, from Lean? Just as hard as going from English to Lean? If it is easier to convert backwards, maybe the AI can at least describe what the equations mean…