[HN Gopher] Learning Lean: Part 1
___________________________________________________________________
Learning Lean: Part 1
Author : vinhnx
Score : 62 points
Date : 2026-02-15 10:20 UTC (3 days ago)
(HTM) web link (rkirov.github.io)
(TXT) w3m dump (rkirov.github.io)
| awesomeMilou wrote:
| It's interesting to see the notes of someone tackling lean who's
| primary occupation is SWE but has a strong background in
| mathematics.
| nextos wrote:
| 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
| jojomodding wrote:
| 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.
| nyrikki wrote:
| > 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...
| hutao wrote:
| > With Prop, I think what you need to dig into is 'non-
| computational' not 'non-computable'.
|
| 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.
| latenightcoding wrote:
| I never hijack non-ai threads to talk about AI, but can anybody
| share their experience using LLMs to code in Coq, Lean, etc.
| lambdas wrote:
| 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
___________________________________________________________________
(page generated 2026-02-18 23:00 UTC)