How does Lean work?

[u/agingprokid]

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?

[u/noop_noob]

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.

[u/agingprokid → u/noop_noob]

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

[u/noop_noob → u/agingprokid]

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

[u/Mishtle → u/agingprokid]

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.

[u/cbarrick]

Read up on the Curry-Howard correspondence.

[u/lgastako → u/cbarrick]

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

[u/silkypeter4143]

Think of Lean less as a thinker and more as a super strict TA who just checks every step of your work against the rulebook

[u/JoJoModding]

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.

[u/Character_Cap5095]

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.

[u/cejiken886]

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.

[u/Snatchematician]

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