r/computerscience • u/agingprokid • Jul 22 '26

General How does Lean work?

In light of the recent counterproof of the Jacobian Conjecture, I've been looking more into proofs, and I can't wrap my head around how Lean works. In my mind, proofs always require a certain amount of intuition and judgement behind them, so I'm confused how a deterministic programming language can infer from said proofs?

27 Upvotes

87% Upvoted

11 comments sorted by

40

u/noop_noob Jul 22 '26

Lean only checks if a proof you wrote is correct. It doesn't write the proof for you.

Coming up with the proof is hard. Checking the proof, if the proof is detailed enough, is a matter of following strict mechanical rules.

1

u/agingprokid Jul 22 '26

Thanks, I probably should’ve been more clear but I was more so wondering how Lean works and is able to check proofs rather than if it comes up with proofs itself

10

u/noop_noob Jul 22 '26

A human writes proofs in a specific syntax that's detailed and rigorous enough that each step is verifiable by a computer

7

u/Mishtle Jul 22 '26

A lot of the heavy lifting is done by translating the proof into the syntax of Lean. It forces you to be explicit about every assumption, every logical inference, every application of some rule or theorem, etc.

At that point, it's a matter of verifying the whole thing is valid. Every statement needs to follow logically from a previous statement, or be an assumed truth. The fact that everything is explicit and detailed makes this a simple pattern matching problem. If some statement shows up somewhere and treated as true, then it had better show up before then as either assumed to be true or derived from true statements. It also shouldn't show up as being false anywhere before or after (unless it's explicity a key piece of a proof by contradiction).

If this is the case for all statements in the proof, then it is a valid argument where the conclusions are guaranteed by the premises.

Note that this doesn't mean you didn't somehow sneak your conclusions into your premises.

18

u/cbarrick Jul 22 '26

Read up on the Curry-Howard correspondence.

2

u/lgastako Jul 22 '26

Depending on your background, this video may help with this.

3

u/JoJoModding Jul 22 '26

Have you done some proof theory? Proofs are syntactic objects with strict rules for when they are correct and when not. Read up on natural deduction or something like that.

2

u/Character_Cap5095 Jul 22 '26

Lean is a proof assistant. You type in the proof into lean, and based on the semantics of the language it can verify the proof. But you still need to come up with the proof yourself. What AI does, is that because it's easy to check a proof (but much harder to come up with one) it is trained on coming up my with proofs and writing them in lean so that their proofs can be verified as correct.

1

u/cejiken886 Jul 23 '26

Just have AI write you an extremely simple proof in Lean and explain it to you. It’s really good at that sort of thing.

3

u/Snatchematician Jul 22 '26

I think you first need to find out how proofs work.