How to read Lean

Stream: general

[Martin Dvořák]

We have plenty of guides on how to write code in Lean, but as far as I know, there are no guides on how to read code in Lean. I don't mean philosophical treatises on the role of computers in research or how to believe machine-checked proofs. I mean a short and straightforward tutorial that we could ship with our Lean projects, allowing people who can't write Lean to understand what we have proved without relying on us to translate our results into informal language (which can go wrong on so many levels).

Lean has an amazing syntax that can effectively communicate mathematical ideas both to computers and to people. However, no matter how intuitive the syntax is, there are still things that need to be learned before one can understand a theorem statement written in Lean. Most tutorials on Lean focus on the "tactical language" (the by DSL) and perhaps assume that the meaning of terms is usually understood using the context and readers' background knowledge. I'm not talking about writing proofs as terms; I mean all the terms in definitions and statements.

I initially thought that the term language could be easily understood by normal mathematicians who had never been exposed to Lean. I was wrong because I took many things for granted — there are many "unknown knowns" in my mind (and probably in your mind, too). For instance, people often don't automatically know that the things in parentheses right after the theorem name are assumptions. They also might not know that they can easily look up the meaning of the ⬝ᵥ operator, for example.

I would like to address these issues in a tutorial on how to read Lean. Do you have any suggestions on how to write it well? I want it to be short and sweet, and not necessarily foolproof.

[Luigi Massacci]

Do you want this to be with or without the infoview?

[Jireh Loreaux]

I mean, I know this is only half the battle, but: isn't this what docstrings are for?

[Frédéric Dupuis]

I think the idea is to have a document for the scenario where, in a relatively near future, we start submitting research papers with some lemmas (or the whole thing!) formalized in Lean, and want to point the referees to some sort of Lean primer that lets them understand at least the lemma statements in the Lean code. I personally think this would be very valuable.

[Xiyu Zhai]

It would be good to have some guidance for latex listings of lean code. Latex is so hard. Lol

[Johan Commelin]

There is a little bit here: https://leanprover-community.github.io/blog/posts/lte-examples/

[Johan Commelin]

Several papers also say something about this. But not a dedicated tutorial on "how to read Lean".

[Martin Dvořák]

Luigi Massacci said:

Do you want this to be with or without the infoview?

Very good question! I primarily want to give a guide on how to read Lean without the Infoview.

I always aim to write a code so that the definitions and the main results are readable without the Infoview.

[Martin Dvořák]

Xiyu Zhai said:

It would be good to have some guidance for latex listings of lean code. Latex is so hard. Lol

Somebody taught me to include Lean code in LaTeX this way:
https://github.com/madvorak/duality/blob/330868bc8b2937d51bfdd953c4f8ee56a33a5092/nonLean/duality.tex#L62
Unfortunately, I am not able to give credits because I forgot who showed it to me.

[Martin Dvořák]

Jireh Loreaux said:

I mean, I know this is only half the battle, but: isn't this what docstrings are for?

I don't think we should write docstrings such that everything can be understood from the docstrings only, not looking at the code at all.

[Martin Dvořák]

Frédéric Dupuis said:

I think the idea is to have a document for the scenario where, in a relatively near future, we start submitting research papers with some lemmas (or the whole thing!) formalized in Lean, and want to point the referees to some sort of Lean primer that lets them understand at least the lemma statements in the Lean code. I personally think this would be very valuable.

Yeah, I also want to get there!
Lean should not be treated as something that accompanies the math.
Lean is the math!

[Johan Commelin]

Nah, I'm too much of a platonist to agree with that statement. Whatever we're doing on paper or in Lean, it's a shadow of the real math.

[Martin Dvořák]

I was thinking which theorems I should use in the demonstrations. What do you think about the following?

Mathlib/Data/Real/Irrational.lean:

def Irrational (x : ℝ) :=
  x ∉ Set.range ((↑) : ℚ → ℝ)

theorem irrational_sqrt_two : Irrational (√2) := by
  simpa using Nat.prime_two.irrational_sqrt

Mathlib/Analysis/Complex/Polynomial/Basic.lean:

theorem exists_root {f : ℂ[X]} (hf : 0 < degree f) : ∃ z : ℂ, IsRoot f z := by
  by_contra! hf'
  /- Since `f` has no roots, `f⁻¹` is differentiable. And since `f` is a polynomial, it tends to
  infinity at infinity, thus `f⁻¹` tends to zero at infinity. By Liouville's theorem, `f⁻¹ = 0`. -/
  have (z : ℂ) : (f.eval z)⁻¹ = 0 :=
    (f.differentiable.inv hf').apply_eq_of_tendsto_cocompact z <|
      Metric.cobounded_eq_cocompact (α := ℂ) ▸ (Filter.tendsto_inv₀_cobounded.comp <| by
        simpa only [tendsto_norm_atTop_iff_cobounded]
          using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop)
  -- Thus `f = 0`, contradicting the fact that `0 < degree f`.
  obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]
  simp at hf

Mathlib/GroupTheory/Coset/Card.lean:

theorem card_subgroup_dvd_card [Group α] (s : Subgroup α) : Nat.card s ∣ Nat.card α := by
  classical simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]

I would show it including the proofs and immediately tell the readers that everything after by can be ignored.

[Martin Dvořák]

Here's my first draft:
https://github.com/madvorak/read-lean

I think I should probably stop using $math$ on GitHub. The absolute values are rendered very ugly. What do you think?

[Martin Dvořák]

PRs are welcome! Forks are strongly encouraged.

Also, please tell me what to do with the ugly TeX-like parts.

[Michael Rothgang]

Starting to read it, I am pausing at the phrasing "calling a lemma". I would perhaps say "applying a lemma"...

[Michael Rothgang]

And I am pausing at the paragraph containing "This operator ↑ takes a rational number and outputs a Cauchy sequence with given rational number on all positions." I'd rather say that ↑ converts a rational number to its corresponding real number. The precise implementation (Cauchy sequences, Dedekind cuts, Eudoxus' definition etc.) is a detail that most mathematicians need not care about - I would rather not emphasize it.

[Michael Rothgang]

Both of these said: I think the README is a nice explanation; thank you for writing it!

[Martin Dvořák]

Michael Rothgang said:

Starting to read it, I am pausing at the phrasing "calling a lemma". I would perhaps say "applying a lemma"...

Wouldn't the phrase "applying a lemma" allude to apply foo then?
Maybe I should change it regardless.
After all, the phrase "calling a lemma" might allude to proof terms, which the reader doesn't care about.

[Martin Dvořák]

Michael Rothgang said:

And I am pausing at the paragraph containing "This operator ↑ takes a rational number and outputs a Cauchy sequence with given rational number on all positions." I'd rather say that ↑ converts a rational number to its corresponding real number. The precise implementation (Cauchy sequences, Dedekind cuts, Eudoxes' definition etc.) is a detail that most mathematicians need not care about - I would rather not emphasize it.

Would you omit both following sentences?

"This operator ↑ takes a rational number and outputs a Cauchy sequence with given rational number on all positions. We decide not to go that deep and trust the Mathlib's implementation of number systems and conversions between them."

Without them, the paragraph flows as follows:

"The operator ↑ denotes this embedding (in fact, it could denote several other embeddings, hence the explicit type annotation ℚ → ℝ is necessary here). We see that x is irrational iff x isn't in the range of the embedding function, i.e, x is a real number that doesn't correspond to any rational number."

[Michael Rothgang]

Martin Dvořák said:

Michael Rothgang said:

Starting to read it, I am pausing at the phrasing "calling a lemma". I would perhaps say "applying a lemma"...

Wouldn't the phrase "applying a lemma" allude to apply foo then?
Maybe I should change it regardless.
After all, the phrase "calling a lemma" might allude to proof terms, which the reader doesn't care about.

Well, "calling a lemma" sounds like "calling a function" to me --- which is clearly not a helpful associatiation. In terms of prose, I'd always "use" or "apply" a lemma - regardless of whether that's called apply or refine in mathlib.

[Michael Rothgang]

Martin Dvořák said:

Michael Rothgang said:

And I am pausing at the paragraph containing "This operator ↑ takes a rational number and outputs a Cauchy sequence with given rational number on all positions." I'd rather say that ↑ converts a rational number to its corresponding real number. The precise implementation (Cauchy sequences, Dedekind cuts, Eudoxes' definition etc.) is a detail that most mathematicians need not care about - I would rather not emphasize it.

Would you omit both following sentences?

"This operator ↑ takes a rational number and outputs a Cauchy sequence with given rational number on all positions. We decide not to go that deep and trust the Mathlib's implementation of number systems and conversions between them."

Without them, the paragraph flows as follows:

"The operator ↑ denotes this embedding (in fact, it could denote several other embeddings, hence the explicit type annotation ℚ → ℝ is necessary here). We see that x is irrational iff x isn't in the range of the embedding function, i.e, x is a real number that doesn't correspond to any rational number."

Good idea! I just looked at the whole paragraph. With some word-smithing, I'd write it as follows:
`
We would like to define irrationals numbers to be the set difference ℝ − ℚ. Unfortunately, we cannot quite write it this way in Lean. Lean isn't based on set theory; Lean uses type theory. Therefore, we cannot say that rational numbers are a subset of real numbers: for example, the rational number 5 and the real number 5 are of different types. Instead, rational numbers are embedded in real numbers: each rational number corresponds to a unique real number. In our example, the operator ↑ denotes this embedding. (In fact, it could denote several other embeddings, thus we must add the explicit type annotation ℚ → ℝ).

We see that x is irrational iff x isn't in the range of the embedding function, i.e, x is a real number that doesn't correspond to any rational number. We check that it agrees with our intuition what "being irrational" means and go on.
`

[Mario Carneiro]

Michael Rothgang said:

Well, "calling a lemma" sounds like "calling a function" to me --- which is clearly not a helpful associatiation.

It kind of is though. I've been using Lean for a long time and I frequently mix up the words "call" vs "apply" and "lemma" vs "theorem" vs "function" because in Lean they are basically the same concept. The syntax of Lean really encourages you to blur the distinction between proofs and programs in many ways.

[Michael Rothgang]

I stand corrected then (and will ponder your comment in more detail later).
Let me just say then: this may confuse mathematicians who did not think about this a lot (such as myself, an hour ago).

[Martin Dvořák]

When we are at it, it is more important to tell the readers how to call functions than to tell them how to apply a lemma. If they want to know what a certain theorem says, they must understand that functions are called in the theorem statement.

[Martin Dvořák]

Michael Rothgang said:

Well, "calling a lemma" sounds like "calling a function" to me --- which is clearly not a helpful associatiation.

This is offtopic in this thread, but you might want to look up the Curry-Howard correspondence.

[David Loeffler]

When we are at it, it is more important to tell the readers how to call functions than to tell them how to apply a lemma.

@Martin Dvořák Who is this document intended to be read by?

If you are hoping to reach out to mathematicians (as opposed to computer scientists), then applying lemmas is definitely much more important than calling (non-proof-valued) functions; and the Curry-Howard correspondence is not something you can assume as "common knowledge".

Yes, if you regularly work with Lean, you quickly get used to the idea that a lemma is a function which returns proofs. But if you regularly work with Lean, you don't need to be reading this document. Having learnt Lean as a mathematician, and subsequently taught Lean to mathematics students, I would say that this idea (proofs as functions) is definitely among the more difficult mental adjustments that needs to be made for a Lean novice, and if you take it for granted it will substantially reduce the value of this document to a big chunk of its potential target audience.

[Martin Dvořák]

The document is intended for people who know math but don't know Lean.
It should allow them to read the results, not to study the proofs.

Given the purpose, we can kick out "applying a lemma" and "calling a lemma" as well.
The only thing that needs to be explained is "calling a function" IMO.

As for the Curry-Howard correspondence, this remark of mine was offtopic.
It is neither going to be assumed nor is it going to be explained in the document.

[Yury G. Kudryashov]

I guess, you can "use" a lemma (applies both to forward and backward deduction). But I may be wrong: English is not my first language.