[sibrahim]

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]

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

[ndriscoll]

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.

[johncolanduoni]

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]

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.

[digikata]

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.

[mrtesthah]

They probably need to be able to read and understand the lean language.

[threatofrain]

It’s far easier for Lean because the human has to read very little compared to generating whole programs.

[luckydata]

the same way you verify that any other program compiles? I don't understand the question tbh, it seems self evident.

[oh_my_goodness]

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

Skilled humans must understand the problem and write the theorem statement.

[f1shy]

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

[exe34]

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]

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.

[heroprotagonist]

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]

No, it can tell you that 42 is the answer to (some lean statement), but not what question that lean statement encodes.

[davidwritesbugs]

I recently learnt that Douglas Adams wrote code and the ultimate answer was '*' - 42 in ascii

[bee_rider]

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…

[rurban]

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]

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.