> Prop vs Decidable - I vaguely understand the distinction, but can use more examples. Also would like to know does this relate to the noncomputable property.
My path to this subject was tortured, so sorry if I don’t account for Polysemy etc.
With Prop, I think what you need to dig into is ‘non-computational’ not ‘non-computable’.
Mere propositions is probably best viewed with Homotopy Type Theory[0]
Two proofs (t1,t2) of the same proposition (p:Prop) which are definitionally equal are proof irrelevant, meaning that all they carry is the proof p is true.
This paper [1] may be helpful but the difference between groupoids and subsingletons with classical mathematics is challenging for many of us.
Hopefully this helps in your journey.
Also remember that with classical set theory the internal and external proposition truths are different, the Curry–Howard correspondence is to constructivist from lambda calculus, you don’t have PEM etc…
Remember DGM[2] shows that finite indexing or projection is PEM
Good luck and I hope you continue to share your journey.
While I don't know the specifics of Lean, I know Rocq and will attempt to answer some of the remaining questions. I look forward to someone else telling me that my intuition from Rocq is completely wrong, so take this all with a grain of salt and read the comments replying to this one.
1) rfl vs doing a proof:
It depends on how your things are defined. For example, consider the function that appends two lists, a classic in functional programming (Here's a refresher: https://stackoverflow.com/a/35442915/2694054 )This is usually defined by recursion. But the details matter: The example in the link is defined by recursion on the first argument. That is, for a concrete first argument, it can evaluate. So it can e.g. evaluate `append [] ys` to `ys` just by unfolding the definition and resolving matches. But for `append xs []` you can not evaluate the `xs` any further because the remaining behavior depends on its concrete shape. So to prove that `append xs [] = xs` you need a proof (by induction).
2) Prop vs Decidable
Prop is a mathematical proposition. For example, the Riemann Hypothesis is a Prop. But a decidable Proposition is one for which you can write a program that knows if it is true or false. And you need to actually write this program, and prove it correct. So currently the Riemann Hypothesis is not decidable, because no one figured out how to write that program yet. (It will be a simple `return true` or `return false`, but which??) This mostly shows up for something like `forall x y, decidable (x = y)` which allows you to say that for any two numbers you can decide if they are equal or not. You can then use this when you actually do functional programming in Lean and actually want to run the program on concrete inputs.
The remaining two questions are more specific to Lean's engineering so I won't even attempt to answer that.
Lean is great, but if someone's primary interest is SWE, I think there are better choices. The Lean community is primarily focused on formalizing mathematics right now. This might change in the future. Lean is nice to learn theorem proving, but once you learn the basics, you'll hit a roadblock when trying to move to software verification applications.
For SWE, the most mature option is probably Isabelle. It's also a classical theorem prover, and it's perhaps easier to start with something that doesn't have dependent types. A cool thing is that the canonical Isabelle book [1] has been rewritten in Lean [2].
I’ve never used them first hand, but crackpots sure do love claiming to solve Riemann hypothesis, P vs NP, Collatz conjecture etc and then peddle out some huge slop. My experience has solely been curiously following what the LLM’s have been generating.
You have to be very, VERY careful. With how predisposed they are to helping, they’ll turn to “dishonesty” rather than just shut down and refuse. What I tend to see is they get backed into a corner, and they’ll do something like prove something different under the guise of another:
They’ll create long pattern matching chains as to create labyrinths of state machines.
They’ll keep naming functions, values and comments to seem plausible, but you have to follow these to make sure they are what they say. A sneaky little trick is to drop important parameters in functions, they appear in the call but not in the actual body.
They’ll do something like taking a Complex value, but only working with the real projection, rounding a number, creatively making negatives not appear by abs etc etc
So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task.
And when it doesn’t work, introducing an error or two in formal proof systems often means you’re getting exponentially further away from solving your problem.
I’ve not seen a convincing use that tactics or goals in the proof assistant themselves don’t already provide
> Prop vs Decidable - I vaguely understand the distinction, but can use more examples. Also would like to know does this relate to the noncomputable property.
My path to this subject was tortured, so sorry if I don’t account for Polysemy etc.
With Prop, I think what you need to dig into is ‘non-computational’ not ‘non-computable’.
Mere propositions is probably best viewed with Homotopy Type Theory[0]
Two proofs (t1,t2) of the same proposition (p:Prop) which are definitionally equal are proof irrelevant, meaning that all they carry is the proof p is true.
This paper [1] may be helpful but the difference between groupoids and subsingletons with classical mathematics is challenging for many of us.
Hopefully this helps in your journey.
Also remember that with classical set theory the internal and external proposition truths are different, the Curry–Howard correspondence is to constructivist from lambda calculus, you don’t have PEM etc…
Remember DGM[2] shows that finite indexing or projection is PEM
Good luck and I hope you continue to share your journey.
[0] https://homotopytypetheory.org/wp-content/uploads/2013/03/ho...
[1] https://jesper.sikanda.be/files/definitional-proof-irrelevan...
[2] https://ncatlab.org/nlab/show/Diaconescu-Goodman-Myhill+theo...
While I don't know the specifics of Lean, I know Rocq and will attempt to answer some of the remaining questions. I look forward to someone else telling me that my intuition from Rocq is completely wrong, so take this all with a grain of salt and read the comments replying to this one.
1) rfl vs doing a proof:
It depends on how your things are defined. For example, consider the function that appends two lists, a classic in functional programming (Here's a refresher: https://stackoverflow.com/a/35442915/2694054 )This is usually defined by recursion. But the details matter: The example in the link is defined by recursion on the first argument. That is, for a concrete first argument, it can evaluate. So it can e.g. evaluate `append [] ys` to `ys` just by unfolding the definition and resolving matches. But for `append xs []` you can not evaluate the `xs` any further because the remaining behavior depends on its concrete shape. So to prove that `append xs [] = xs` you need a proof (by induction).
2) Prop vs Decidable
Prop is a mathematical proposition. For example, the Riemann Hypothesis is a Prop. But a decidable Proposition is one for which you can write a program that knows if it is true or false. And you need to actually write this program, and prove it correct. So currently the Riemann Hypothesis is not decidable, because no one figured out how to write that program yet. (It will be a simple `return true` or `return false`, but which??) This mostly shows up for something like `forall x y, decidable (x = y)` which allows you to say that for any two numbers you can decide if they are equal or not. You can then use this when you actually do functional programming in Lean and actually want to run the program on concrete inputs.
The remaining two questions are more specific to Lean's engineering so I won't even attempt to answer that.
It's interesting to see the notes of someone tackling lean who's primary occupation is SWE but has a strong background in mathematics.
Lean is great, but if someone's primary interest is SWE, I think there are better choices. The Lean community is primarily focused on formalizing mathematics right now. This might change in the future. Lean is nice to learn theorem proving, but once you learn the basics, you'll hit a roadblock when trying to move to software verification applications.
For SWE, the most mature option is probably Isabelle. It's also a classical theorem prover, and it's perhaps easier to start with something that doesn't have dependent types. A cool thing is that the canonical Isabelle book [1] has been rewritten in Lean [2].
[1] http://concrete-semantics.org
[2] https://github.com/lean-forward/logical_verification_2025
I never hijack non-ai threads to talk about AI, but can anybody share their experience using LLMs to code in Coq, Lean, etc.
I’ve never used them first hand, but crackpots sure do love claiming to solve Riemann hypothesis, P vs NP, Collatz conjecture etc and then peddle out some huge slop. My experience has solely been curiously following what the LLM’s have been generating.
You have to be very, VERY careful. With how predisposed they are to helping, they’ll turn to “dishonesty” rather than just shut down and refuse. What I tend to see is they get backed into a corner, and they’ll do something like prove something different under the guise of another:
They’ll create long pattern matching chains as to create labyrinths of state machines.
They’ll keep naming functions, values and comments to seem plausible, but you have to follow these to make sure they are what they say. A sneaky little trick is to drop important parameters in functions, they appear in the call but not in the actual body.
They’ll do something like taking a Complex value, but only working with the real projection, rounding a number, creatively making negatives not appear by abs etc etc
So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task.
And when it doesn’t work, introducing an error or two in formal proof systems often means you’re getting exponentially further away from solving your problem.
I’ve not seen a convincing use that tactics or goals in the proof assistant themselves don’t already provide