Learning Lean: Part 1

https://rkirov.github.io/posts/lean1/

by vinhnx • 5 months ago

131 16 5 months ago

rkirov.github.io

It's interesting to see the notes of someone tackling lean who's primary occupation is SWE but has a strong background in mathematics.

nextos2• 5 months ago

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

nextos2• 5 months ago

If verification is the goal, but you don't want to learn theorem proving yet, Dafny is really approachable and practical [1]. F* is also worth considering as a proof-oriented alternative to Isabelle that is focused on software verification [2]. Why3, Rocq and Agda are other obvious contenders.

[1] https://dafny.org/latest/OnlineTutorial/guide

[2] https://fstar-lang.org/tutorial

gaogao• 5 months ago

The future is now. The recent couple of Lean releases have leaned more on software verification, I believe in part due to Amazon hiring a number of the core devs.

jojomodding• 5 months ago

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• 5 months ago

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• 5 months ago

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• 5 months ago

I never hijack non-ai threads to talk about AI, but can anybody share their experience using LLMs to code in Coq, Lean, etc.

lambdas2• 5 months ago

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

adamddev1• 5 months ago

introducing an error or two in formal proof systems often means you’re getting exponentially further away from solving your problem

I wish people understood that this is pretty much true of software building as well.

trevyn• 5 months ago

So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task.

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

If I construct a term of this type without going via one of the (fairly obvious) soundness holes or a compiler bug, it's very likely proved, no? No matter how inscrutable the proof is from a mathematical perspective. (Translating it into something mathematicians understand is a separate question, but that's not really what I'm asking.)

christoff12• 5 months ago

I thought this was about Toyota's Lean when I clicked lol.

That's catnip for my original IE brain.

jsmo• 5 months ago

Thank you

xiaodai• 5 months ago

i am a mathematician wanna-be. I have an undergrad honours degree in maths. As a retirement or pre-retirement project, I want to learn LEAN and contribute to it either via development or via developing the Mathlib or both!

Pointers welcome. As long as they are not null. Btw, I am also interested in compilers.

Learning Lean: Part 1

Related Stories