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_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 and the lemma
cos_two_neg is the lemma that . 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 has a zero between and . We define 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 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 to ten decimal places (and a computer to far more if necessary), and then one could compute the value of to ten decimal places (or to far more) and see that it is .
But Lean is different. Lean is not a calculator. Lean is a theorem prover. It is true by definition that in Lean, and it is a theorem in Lean that and hence it is a theorem in Lean that . 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 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 with no numerical computation at all.
But what if one did want to do a numerical computation of ? 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 “, but actually what does it know about the value of ? Well, by definition, is twice a number between 1 and 2, so we get
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
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 and ? Floris used the following trick:
Using this standard fact, and the fact that , he could deduce exact values for . Because he could deduce exact values for . He could also prove that if then (by using the power series for and the fact that when ) and as a consequence could prove lower bounds for ! By using two terms of the power series for sine we can also prove that for 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 to 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 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.