Here’s one of my favorite theorems from geometry, both because of the result itself, and because of the proof I’ll describe in this blog post. I suspect it was much better known when spherical trigonometry used to be part of the standard curriculum, but that was before my time. Now it seems to be forgotten, and if it’s mentioned at all it’s in a differential geometry course as an elementary consequence of the more general and powerful Gauss-Bonnet theorem.

One of the very old and well known results about triangles is that the sum of the angles is equal to (or if you measure angles in degrees instead of radians, which is almost never done in modern mathematics). Girard’s theorem can be viewed as the analogous result in the context of spherical geometry, where the analogue of line segments in the plane is great circle arcs on the sphere.

**Girard’s Theorem** For a spherical triangle on a unit sphere (i.e. radius equal to one) with interior angles the quantity is equal to the area of the triangle.

The way this is proved nowadays (which is **not** the proof I’ll discuss later in this post) is by first proving the Gauss-Bonnet theorem. To do that you need to work in the more general context of Riemannian geometry where lines in a plane generalize to geodesics in a surface (or an dimensional Riemannian manifold if you really want to generalize). And then you need to introduce the concept of curvature.

Once you’ve done all that, you can finally state and prove the Gauss-Bonnet theorem, which says that the quantity (where the curves that make up a triangle are geodesics) is equal to the integral of the curvature over the surface of the triangle. For a unit sphere the curvature is one, and for the plane the curvature is zero, and so the Gauss-Bonnet theorem can be used to prove both results mentioned above.

Just as there’s a much more direct and elementary proof of the result for planar triangles, there’s a much more direct and elementary proof of the result for spherical triangles, and that’s what I’ll write about in this post.

To warm up for the proof, I’d like to discuss the solution to a seemingly unrelated combinatorial problem. It turns out to be very closely related, since an approach to solving it is exactly the same as an approach to proving Girard’s theorem.

**Problem** Consider all words consisting of three characters How many words of length three are there where all three characters occur?

The answer is of course six, namely the permutations

There’s another way to solve this problem, and I want to describe it at length because the same idea is going to be used to prove Girard’s theorem. The approach is to consider the words of length three where **exactly two** of the characters occur, and to count them in two different ways, both of which involve the answer to the combinatorial question above i.e. the number of words of length three where all three characters occur.

And, since we want to solve for the number of words of length three where all three characters occur, let’s give it a name And, of course, to repeat, we know that from the enumeration argument above, but we’re going to proceed without that knowledge.

The first thing to consider is the number of words of length three that have **at least two** of the characters. Call that number .

This means that the number of words of length three that have **exactly two** of the characters must be

Now for the other way of counting. Consider the total number of three letter words that contain each of the characters (and may or may not contain ). Call it . Similarly, let’s use for the number of words containing and for the number of words containing

The total number of words of length three that have **exactly two** of the characters must be

and so by solving for in the equality

we have another way of computing W

is , since there are words of length three, and only of them don’t have at least two of the three characters, namely

is . There are two words that start with namely . There are five words that start with since there are three that start with , one that starts with , and one that starts with . And if there are five that start with there must be five that start with since the roles of and are symmetrical. Twelve is two plus five plus five.

Similarly, and are each equal to

So we have

which gives us

Now let’s prove Girard’s theorem.

We have a spherical triangle with angles Consider the continuation of the sides that generate the angle . And by “continuation”, I mean continuing each side all the way around the sphere until it reaches itself by forming a great circle. We get a region consisting of two “wedges” or “lunes” of total area

Now do the same for and , to get regions of area and

The three regions cover the sphere, and their intersection is the spherical triangle , together with its antipodal triangle . And, importantly, the intersection of any two regions is the same as the intersection of all three (just like with the combinatorial situation).

So, just as with the combinatorial situation above, we have

and have the same area and are disjoint, so that , and so that we have

which gives us