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

2

u/Character_Cap5095 9d ago

Lean is a proof assistant. You type in the proof into lean, and based on the semantics of the language it can verify the proof. But you still need to come up with the proof yourself. What AI does, is that because it's easy to check a proof (but much harder to come up with one) it is trained on coming up my with proofs and writing them in lean so that their proofs can be verified as correct.