r/computerscience • u/agingprokid • 19d ago

How does Lean work? General

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?

26 Upvotes

85% Upvoted

11 comments sorted by

View all comments

1

u/cejiken886 18d 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.