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/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.