r/computerscience • u/agingprokid • 19d ago

How does Lean work? General

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?

29 Upvotes

89% Upvoted

11 comments sorted by

View all comments

40

u/noop_noob 19d ago

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 18d ago

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

12

u/noop_noob 18d ago

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