# Has there been any attempt at a tutorial that doesn't start with natural numbers?

The most well-known tutorials/learning materials, including Book 1, Chapter 2 of Software Foundations for Coq and the Natural Number Game for Lean, use natural numbers to introduce induction. But there are multiple complaints by new learners that having to prove trivial facts of natural numbers via induction feels unintuitive and intimidating (one example).

Has there been any attempt at a tutorial that doesn't start with natural numbers? I can imagine using monomorphic lists instead, say a list of booleans. For example, proving associativity of list concatenation (a ++ b) ++ c = a ++ (b ++ c) should feel less intimidating (because it is no longer a "trivial" property of natural numbers the students would have taken as granted) and more interesting than proving associativity of addition on natural numbers. And then the properties of natural numbers could be introduced by pointing to similarities with list operations.

• Some people have worked on Real Number Game for Lean, but I think it has NNG as a "prerequisite", so probably doesn't quite classify as an answer. Feb 8 at 23:57
• To me associativity of list concatenation seems more trivial that associativity of addition of natural numbers. It's not really possible to understand the statement of associativity of list concatenation without understanding why it's true, while that is possible for associativity of addition of natural numbers. Feb 8 at 23:57

Patrick Massot's very nice tutorial for Lean takes place in the domain of elementary (epsilon-delta) real analysis. As a mathematician but not a mathematician focused on foundations, this to me feels like a very sensible place to start.

• I guess "don't teach induction at all" is probably a valid answer (I checked the entire repo and induction is used only once for a given lemma), but I'd prefer one that actually teaches induction but not with natural numbers (if such a thing exists). Feb 9 at 0:20
Joseph Hua, Ken Lee, and Bendit Chan have recently released the HoTT Game, designed as an introduction to Cubical Agda for mathematicians with no proof verification experience. The two parts of this tutorial are Trinitarianism (nicely summarized here) which introduces all the basic notions of (homotopy) type theory, and Fundamental Group of the Circle, whose goal is showing that $$\pi_1(S^1)\cong\mathbb Z$$.
Granted, at some points working with $$\mathbb Z$$ reduces to working with (two copies of) $$\mathbb N$$, but unlike the tutorials mentioned in the original post, the theorems of this tutorial are not about arithmetic of $$\mathbb N$$.