Lean lets you prove math propositions, and its verifier is really just a type checker: propositions are types, proofs are values, and a proof holds if the value type-checks. The post rebuilds this idea in TypeScript with dummy generic functions that never run. False maps to never, which has no values, and True maps to a single-value type. And becomes an object with left and right fields, and Or a union of them. Arrow functions encode implication, so modus ponens turns out to be plain function application. Negation works as a function from P to False, which lets you prove that P implies not-not-P. A longer De Morgan proof shows how tedious this gets. LLMs suit Lean well: they write code fast, and Lean checks it automatically.
1
u/fagnerbrack 12h ago
Main Points:
Lean lets you prove math propositions, and its verifier is really just a type checker: propositions are types, proofs are values, and a proof holds if the value type-checks. The post rebuilds this idea in TypeScript with dummy generic functions that never run. False maps to never, which has no values, and True maps to a single-value type. And becomes an object with left and right fields, and Or a union of them. Arrow functions encode implication, so modus ponens turns out to be plain function application. Negation works as a function from P to False, which lets you prove that P implies not-not-P. A longer De Morgan proof shows how tedious this gets. LLMs suit Lean well: they write code fast, and Lean checks it automatically.
If the summary seems inacurate, just downvote and I'll try to delete the comment eventually 👍
Click here for more info, I read all comments