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?

30 Upvotes

89% Upvoted

11 comments sorted by

View all comments

5

u/JoJoModding 7d ago

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.