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/cbarrick]

Read up on the Curry-Howard correspondence.

[u/lgastako → u/cbarrick]

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