Learning Lean: Part 1
rkirov.github.io
rkirov.github.io
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...
Here's another way to explain this:
As you state, Prop has to do with proof-irrelevance. When doing constructive mathematics, proofs are programs (meaning they carry computational content), but sometimes it's useful to treat any two proofs of the same proposition as equal. As a consequence, proofs cannot be inspected or run as programs, and you get back the Law of Excluded Middle from classical mathematics.
Decidable has to do with decidability. This means that given some proposition P, there is an algorithm that can either produce a proof of P, or a proof of ~P. This is usually useful when P is a predicate, so that at each x, P(x) either has a proof or a disproof.
In classical mathematics, the Law of Excluded Middle holds for all propositions. In constructive mathematics, the Law of Excluded Middle only holds for decidable propositions. If P is decidable, it is safe to constructively assume P or ~P because an algorithm can produce the answer.
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.
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
Pointers welcome. As long as they are not null. Btw, I am also interested in compilers.
That's catnip for my original IE brain.
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
I wish people understood that this is pretty much true of software building as well.
Is this true?
e.g. the Riemann hypothesis is in mathlib:
def RiemannHypothesis : Prop :=
∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2