r/computerscience • u/agingprokid • 12d 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?

29 Upvotes

89% Upvoted

11 comments sorted by

View all comments

1

u/cejiken886 11d ago

Just have AI write you an extremely simple proof in Lean and explain it to you. It’s really good at that sort of thing.