Happy pi day

Yesterday was pi day, and discussion of Lean’s support of pi came up on the chat. The discussion of pi is I think a great way of illustrating what Lean can and cannot do.

To start with, “Lean has pi”. Here it is in the source code.

lemma exists_cos_eq_zero : ∃ x, 1 ≤ x ∧ x ≤ 2 ∧ cos x = 0 :=      real.intermediate_value'       
(λ x _ _, continuous_iff_continuous_at.1 continuous_cos _)
(le_of_lt cos_one_pos)
(le_of_lt cos_two_neg) (by norm_num)

noncomputable def pi : ℝ := 2 * classical.some exists_cos_eq_zero

If you have ever thought about how pi might be defined formally, then maybe you can see what is going on here. The lemma cos_one_pos is the lemma that cos(1)>0 and the lemma cos_two_neg is the lemma that cos(2)<0. Cosine is defined as a power series and these are grotty power series computations. Now using the fact that cosine is continuous, and the intermediate value theorem, we can prove that cos(x) has a zero between x=1 and x=2. We define \pi to be two times an arbitrary zero of the cosine function between 1 and 2 (we choose a random one, using the computer science version of the axiom of choice, which says that you can choose an element from a non-empty set — just don’t get me started on this). The library then goes on to prove that in fact the cosine function has a unique zero in this range (because the cosine function is decreasing in this range) and now we have an unambiguous definition of \pi in Lean.

One has to constrast this approach with an approach taken by, say, a hand calculator, or a programming language like python or C++. In these languages, a value for pi will either be hard coded, or there will be an algorithm implemented which will generate pi to an arbitrary precision in as quick a time as possible. So, for example, a calculator can typically produce the value of \pi to ten decimal places (and a computer to far more if necessary), and then one could compute the value of \sin(\pi) to ten decimal places (or to far more) and see that it is 0.000000\dots.

But Lean is different. Lean is not a calculator. Lean is a theorem prover. It is true by definition that \cos(\pi/2)=0 in Lean, and it is a theorem in Lean that \sin(2\theta)=2\sin(\theta)\cos(\theta) and hence it is a theorem in Lean that \sin(\pi)=0. Note however that Lean has not done any numerical computation to prove this, it has deduced it from theorems and definitions. For this kind of question, one could regard Lean as performing better than the traditional “computational” model of a computer that we have — a computer can check that \sin(\pi) is zero to 10 or 1000000 decimal places, and the more places you want, the longer it would take. But it cannot prove the answer is zero. Lean can prove that \sin(\pi)=0 with no numerical computation at all.

But what if one did want to do a numerical computation of \pi? Well, this is the flip side of the story. Lean is not designed for this sort of question at all! It is a computer program which “knows \pi“, but actually what does it know about the value of \pi? Well, by definition, \pi is twice a number between 1 and 2, so we get

Theorem. 2<\pi<4.

So as you can see, in this regard Lean is lagging a bit behind the a hand calculator. It seemed like pi day was a good day to make things better.

And by the end of it, things had got about an order of magnitude better! Thanks to the efforts of Floris van Doorn, with some help by others, we now have

Theorem. 3.14<\pi<3.15.

Ongoing work by Kenny Lau might give us even more decimal places within the next day or so. But how might one go about proving such a theorem, given only a bunch of standard theorems about sine and cosine, and the facts that \cos(\pi/2)=0 and 2<\pi<4? Floris used the following trick:


Using this standard fact, and the fact that \cos(\pi/2)=0, he could deduce exact values for \cos(\pi/4),\ \cos(\pi/8),\ \cos(\pi/16),\ldots. Because \sin(x)^2+\cos(x)^2=1 he could deduce exact values for \sin(\pi/4),\ \sin(\pi/8),\ \sin(\pi/16),\ldots. He could also prove that if x>0 then \sin(x)<x (by using the power series for x\le 1 and the fact that \sin(x)\le 1 when x>1) and as a consequence could prove lower bounds for \pi! By using two terms of the power series for sine we can also prove that \sin(x)>x-x^3/6 for 0<x<1 and this gives us upper bounds.

Taking a random rational number and then squaring it, doubling it and subtracting one (which one has to do to get from \cos(x) to \cos(x)^2 can get a bit hairy once one has done it a few times. Lean had to prove intermediate goals such as

(2 : ℝ) ≤ ((((2 - (157 / 50 / 2 ^ (4 + 1)) ^ 2) ^ 2 - 2) ^ 2 - 2) ^ 2 - 2) ^ 2

and these are real numbers, which in Lean are big complicated equivalence classes of Cauchy sequences, so this looked a bit daunting at first — another reminder that Lean is designed to do proofs, not numerical computations. The norm_num algorithm strained a bit with these checks, however Mario Carneiro pointed out that with judicious approximations one can make life easier: the trick is to constantly replace fractions with large numerators and denominators with approximately equal fractions with smaller numerators and denominators before you square again. These dirty hacks got us through in the end.

The festivities are documented on the pi day thread at the Zulip chat (login required) or the archive of the Zulip chat (no login required), and Floris’ code is here (permalink) or get it at https://github.com/fpvandoorn/mathlib/blob/pi/src/data/real/pi.lean .

Using the decimal expansions library currently being developed by Calle Sonne and myself at Imperial, we can now prove that the first two digits of \pi after the decimal point are 1 and 4. We still have some way to go before we can catch up with Emma Haruka Iwao, but what if her code contains bugs? We have proofs 🙂

In fact in 2017, Bertot, Rideau and Thery did much better — they use Coq to get a million decimal places of pi, formally verified. Doing this work today made me understand far better what an achievement that was.


About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in Uncategorized and tagged , . Bookmark the permalink.

2 Responses to Happy pi day

  1. DT says:

    What are the obstacles to formalizing the definition of pi I learned in school? Circumference divided by diameter.


    • xenaproject says:

      That’s an interesting question! The short answer is: circumference 🙂 Let’s say we can define the length of a straight line. How then do you define the length of a curve, such as the circumference of a circle?

      Method 1: get a piece of string, wrap it round the circumference, straighten it out, and measure that. This is of course no good — it relies on real world physical objects like string, so is unformalisable.

      Method 2: attempt to formalise the above approach. Consider a circle of radius 1. Approximate the circumference by a bunch of straight lines, e.g. by putting N dots around the circle, say, equally spaced, and drawing N straight lines between them making an N-sided polygon. Measure those straight lines, add them all up, and then take the limit as N goes to infinity. Well, now you have to prove a theorem saying that this limit exists. If you do the maths in a manner which a 17 year old schoolkid would do, you find that what you need to prove is that the limit, as N tends to infinity, of 2N*sin(pi/N) exists, and its limit will be the circumference, but wait a minute, I thought we were trying to _define_ pi here, so how come there is a pi in the left hand side as well, when we haven’t even defined it yet? The reason is that the *definition* of sin(x) in Lean is the infinite series x-x^3/3!+x^5/5!-x^7/7!+…, and so the statement sin(theta) equals opposite over hypotenuse involves coming up with a *definition of angle*, and then using standard facts about e^{i.theta} to prove the *theorem* that sine = opposite over hypotenuse. And when you’re defining angle, you need to figure out the angle represented by a whole turn, which is the smallest positive real solution to sin(x)=0 and cos(x)=1, which one can prove is 2*pi from Lean’s definition of pi. I think that if you put this all together you can indeed prove that the two definitions are equal; one will have to prove that the limit of sin(x)/x as x tends to 0 is 1, which as far as I know is not in Lean’s maths library, but which should certainly be possible to prove given what we have. Really we should be proving that the derivative of a convergent power series is what you think it is, but this still isn’t there. So this route should work — but as you can see, it is quite a treacherous path. If pi were defined to be circumference over diameter then it would be very hard to use the definition to do anything, and would involve a big diversion into defining angles. Note that the definition of angles I was given at school, namely that x radians is the length of the arc of the unit circle subtended by angle x involves the same issue with working out the length of a curve.

      Method 3 (the method which will ultimately be used): realise that method 2 is just actually part of the definition of an integral. Define line integrals (integral of ds along a path P from a to b), and then define the circumference as the integral. Define pi to be half this (because the diameter is 2). This is what we will do in the long run, I guess; we have derivatives now, and integrals will be next. It’s interesting to note that whilst algebra in Lean rushes ahead in leaps and bounds, with graduate level algebra now being done, we are still missing some basic undergraduate level analysis. This will slowly appear over the next year or two. This approach using integrals will give a definition, and a robust API for
      integrals will show that the limit used in method 2 will indeed tend to the integral, thus giving an equality between the two definitions.

      Of course, for teaching purposes, one should use the circumference over diameter definition of pi. But when formalising, it seems to me that the definition in Lean is clearly the better one, because it can be introduced much earlier. One only needs continuity of the cosine function and the intermediate value theorem, rather than a robust theory of path integrals.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s