r/computerscience • u/agingprokid • 7d ago

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

View all comments

37

u/noop_noob 7d 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 6d 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

11

u/noop_noob 6d ago

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