if i were to write a post about Lean (the theorem proving language), what would be interesting to cover? i suppose the first question many might have is “why do i need this“ and the answer is “you don’t”, i’m not really trying to sell you on math. but is there something specific you’d want to know
Comments
I feel like I don't have a mental model of what Lean (and especially Lean compiler) is.
z3 calls itself a "theorem prover", as does Lean, but iiuc they aren't really the same thing. I'd be interested to know more about the difference between the two
Lean is an interactive theorem prover, it is guided by human intuition/insight;z3 is a model checker, it brute forces a problem.
Does it require deeper math knowledge?
I can usually work backwards from examples to see what to study more, and I enjoy them whether or not I have an immediate need.
- proofs as "values" of proposition "types"
- types can be parameterized by values
- False as a type with no values
- X → Y means "X implies Y" but also "a function from X to Y" and also "X and Y are parameters" because all of these are equivalent
I'm used to "X => Y" being equivalent to "(not X) or Y"
How do X and Y become sets with all elements of X associating with some element of Y?
...so I'd like to know more about that one please
> Was there something specific that you were hoping to learn / find?
There are some mentions of Lean in this 2024-08 "The Future of TLA+" thread: https://news.ycombinator.com/item?id=41382828
Beyond that, perhaps typed holes as derivatives of types?
That’s fine, unless you want to use the thing.
Why use the thing at all?
Is almost never explained in any kind of practical way.
Perhaps a non-trivial real world use case?
Your favourite to start?
Not a sales pitch.
For fun I can respect it, like building a pds in bash or something. But seems like there are serious attempts which is wild to me