Help getting started

Stream: new members

[Kate]

Hey everyone, I've worked through most of the natural number game and am wondering if those theorems/tactics are available in a library for use in Lean 4 or do I write them myself? I assume its a Mathlib library but finding it difficult to navigate all the documentation. Thanks!

[Zhang Qinchuan]

After NNG, you can read TPIL and MIL:

1. TPIL: https://leanprover.github.io/theorem_proving_in_lean4/
2. MIL: https://leanprover-community.github.io/mathematics_in_lean/

[Vlad Tsyrklevich]

The tactics are standard (except for simp_add), many of the theorems have the same names in Mathlib under the Nat namespace, e.g. Nat.add_comm.

[Kevin Buzzard]

Yes don't use the natural number game repo as a place to continue after NNG (unless you want to help develop the game by writing some more levels). Lean's standard maths library is mathlib, it can do all NNG can do and much much more:

import Mathlib

example (a b : ℕ) : a + b = b + a := by
  rw [Nat.add_comm]
  -- don't need `rfl` because Lean's default `rw` tries `rfl` when it's finished!

example (a b c d : ℕ) : a + c + d + b = b + a + c + d := by
  omega -- tactic which I don't talk about in NNG but which is more powerful than `simp_add`

example (a b : ℕ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  ring -- another tactic which I don't talk about in NNG but which is more powerful than `simp_add`

-- and mathlib has a bunch of other stuff too

-- let X be a topological space
variable (X : Type) [TopologicalSpace X]

-- the identity map from X to X is continuous
example : Continuous (id : X → X) := by
  continuity -- tactic for continuity

-- etc etc

[Kalle Kytölä]

Kevin's answer is correct, but it doesn't tell you how to learn to navigate Mathlib --- which I interpret was implicitly a part of your original question, and which indeed is not a trivial thing at all. Mathlib navigation very much relies on tools other than the documentation, including tactics exact?, simp?, hovers in VS Code, Go to definition, guessing lemma/definition names, #check, #synth, etc.

For starting to learn those, an excellent resource after the NNG is Kevin's own Formalising Mathematics course. To start playing that, you can clone the course repository.