Section 2 : An introduction to the real numbers

The real real numbers

Lean’s maths library mathlib has the real numbers. This isn’t surprising, a lot of programming languages like Python etc have the real numbers. But actually there is a difference between Python’s real numbers and Lean’s real numbers. Python’s real numbers are actually what a computer scientist would call float s, i.e. floating point numbers. Are floating point numbers different to real numbers? Yes, definitely! There are only finitely many floating point numbers, for example. Floats are “real numbers stored up to a finite precision”. Addition on floats is not associative; if N is a really large floating point number and ε is a really small floating point number, then N+ε=N because of rounding errors, so (-N)+(N+ε)=0 but ((-N)+N)+ε=ε.

Lean’s real numbers are the real real numbers. Lean’s real numbers are defined under the hood as equivalence classes of Cauchy sequences (although you will never need to know this). You can prove that Lean’s real numbers are uncountable. Remember that in Lean, we use types not sets. So the real numbers are a type. They have an official name of real, but we never use this; we always use the notation, which is ℝ. Type this in VS Code with \R.

Lean’s maths library mathlib doesn’t just have the real numbers – it also has what is known to computer scientists as an “Application Programming Interface” for the real numbers, otherwise known as an “API” or “interface”. This sounds extremely intimidating, until you discover what this actually means in practice: it means that Lean knows a whole bunch of theorems about the real numbers (for example, a nonempty bounded set of reals has a least upper bound), and Lean also has a whole bunch of definitions of standard functions on the real numbers like the cosine function real.cos : ℝ → ℝ and the square root function real.sqrt : ℝ → ℝ and so on, and it knows a bunch of theorems about these functions too.

Garbage in, garbage out

Did you spot what looked like a mistake in what I just said? I just claimed that the mathlib function real.sqrt took in a real number and outputted a real number. So what happens if you feed in -1 or some other negative number? Lean doesn’t give you an error! It just spits out some arbitrary answer – for all I know, real.sqrt(-1) = 37. I have no idea what real.sqrt(-1) actually is, and it doesn’t even matter, because I am a mathematician, so I only run real.sqrt on non-negative real numbers. If I want to take the square root of a negative number, I use complex.sqrt. Perhaps you are worried that such a cavalier attitude towards square roots of negative numbers leads to contradictions in the system – but it does not. The simplest way to explain why is the following. Let me define a function f on the real numbers, by f(x)=sqrt(x) for x>=0, and f(x)=37 if x<0. Does defining such a function lead to a contradiction in mathematics? Of course it does not! That’s what real.sqrt looks like (although they might have chosen 0 or sqrt(-x) for the output when x was negative – who knows, and who cares). The trick is that it is in the theorems about real.sqrt where the hypotheses of nonnegativity appear. For example, it is probably not true that real.sqrt(a*b)=real.sqrt(a)*real.sqrt(b) in general, because a or b might be negative. However it is true that real.sqrt(a*b)=real.sqrt(a)*real.sqrt(b) if a ≥ 0 and b ≥ 0, and this is the theorem in the library. So you do have to check that you’re not taking the square roots of negative numbers – just not where you might expect.

Lean is not a computer

The last thing I would like to say about the real numbers in this introduction is that Lean 3 is not designed to compute. This might all change in Lean 4, but right now you cannot try and “evaluate” real.sqrt 2 and expect the answer to be equal to 1.41421356.... That ... has no meaning in Lean, because real numbers have infinite precision. You could prove that 1.41421356 < real.sqrt 2 < 1.41421357 and right now you would have to do this manually by squaring up and multiplying out. I think it would be an interesting and possibly tricky challenge to prove something like 0.54 < real.cos 1 ∧ real.cos 1 < 0.55 (Lean’s cosines are of course in radians; one might want to try and prove this using the power series expansion of cosine but it might well be painful).

Working with reals

How do we state that 2+2=4? We can do it like this:

example : (2 : ℝ) + 2 = 4 :=
begin
  sorry
end

What’s going on here? If I hadn’t put that ℝ in there, Lean would have assumed that I meant the natural number 2 – Lean’s “default” 2. The naturals, integers, rationals, reals and complexes (and p-adic numbers for all primes p, if you know what they are) are all different types, so they all have different 2 s. Writing (2 : ℝ) tells Lean exactly which 2 we mean.

So how come we didn’t have to write (2 : ℝ) + (2 : ℝ) = (4 : ℝ)? The reason for this is that addition in Lean takes two terms of a type X and outputs a term of the same type X, so once Lean knows that the first term has type ℝ it figures out that all the other terms must have type ℝ as well for things to make sense.

How do we prove that 2+2=4? The answer is the norm_num tactic, which “normalises numerical expressions” – in other words it proves equalities and inequalities as long as only numbers, and no variables, are involved.

To solve the sorry s in section 2 you’ll need to know about the norm_num and ring tactics, as well as the specialize tactic. Read about them in the tactic documentation in Part C, and, if you like, in the mathlib community tactic documentation .