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_two_neg is the lemma that 
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 
But Lean is different. Lean is not a calculator. Lean is a theorem prover. It is true by definition that 
But what if one did want to do a numerical computation of
Theorem. 
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. 
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
Using this standard fact, and the fact that 
Taking a random rational number and then squaring it, doubling it and subtracting one (which one has to do to get from 
(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
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.
Xena 
What are the obstacles to formalizing the definition of pi I learned in school? Circumference divided by diameter.
LikeLike
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.
LikeLike