Playing with AlphaGeometry

In my previous post on Euclidea’s Chord Trisection problem, I discovered that AlphaGeometry could prove why the construction worked without needing any auxiliary points. This got me hooked on using AlphaGeometry to understand other mysterious Euclidea solutions.

Today I’m tackling the 8E solution of Point Equidistant from Side of Angle and Point - Problem 13.5 from the Nu pack. Like the chord trisection problem, the optimal solution is a little difficult to follow and the wiki offers no explanation for why it works.

Impressions on AlphaGeometry

The idea is excellent. The execution is garbage.

To run this thing successfully, you need to be:

1. A programmer with linux/gpu experience
2. A decent mathematician
3. An excellent debugger
4. Someone with way too much free time

The input language is opaque and barely documented. Requires a specific platform. No UI. Sometimes crashes when the LLM suggests an invalid auxiliary point. I spent 20 hours reading their white paper, reverse-engineering examples, debugging source code, and watching runs crash after 4 hours. Had to modify their codebase just to work on macOS instead of needing a specific linux distro with GPUs.

This reeks of software written by mathematicians who can code but have never shipped something people will actually use. One week from a real software engineer could turn this into something incredible. Instead we get this.

(For future reference for me, the docs for Newclid were actually more helpful than AlphaGeometry resources. See: JGEX definitions, Predicates)

But after putting in those 20 hours… yeah, it works. Not just works - it rocks!

Euclidea Problem 13.5

Construct a point on segment $\overline{AB}$ that is equidistant from point $M$ and line $BC$.

The 5L Solution

The 5L solution is pretty sleek. Weirdly, it’s the solution that I was able to get even though it’s arguably harder than the 8E solution. You decide. It’s also Exercise 4.2 in Lectures on Euclidean Geometry - Volume 1 by Paris Pamfilos.

The idea is to recognize that $E$ is the center of a circle tangent to $\overline{BC}$ and going through $M$. Then use power of a point on a point whose power is known. That point happens to be where a perpendicular to $\overline{AB}$ through $M$ intersects with $\overline{BC}$:

Notice how no matter where the tangent point $D$ happens to be, $\overline{PM}$ is known and constant, and $\overline{PM'}$ is known and constant. Therefore, we can compute the power of this point, which is $(\overline{PM})(\overline{PM'})$. On the other hand, the power of the point is also $(\overline{PD})^2$. Therefore length $\overline{PD}$ is $\sqrt{\overline{PM} \cdot \overline{PM'}}$, in other words the geometric mean of $\overline{PM}$ and $\overline{PM'}$. Many people know one way to construct the geometric mean of two segments, but I’ll introduce a second handy one that’s less used:

Since the problem is already set up to use the overlapping geometric mean construction, we can go ahead and use that to get length $\overline{PD}$ and finish the problem. Note that the actual 5L solution has a cool optimization where it actually draws $M'$ above $P$ instead of below line $\overline{AB}$.

The 8E Solution

Here’s the solution from the wiki:

1. Select arbitrary point F between A and B on line AB.
2. Construct circle F with radius FB intersecting line BC at G and line AB at H.
3. Construct circle H with radius HG.
4. Construct line BM intersecting circle H at I with I being farthest from B.
5. Construct circle I with radius IM intersecting line BM at J.
6. Construct a second circle H with radius HJ intersecting circle I at K.
7. Construct line KM intersecting line AB at E.
8. Construct circle E with radius EM tangent to BC at D.
9. Construct line DE. Segments DE and EM are the desired result.

I don’t know about you, but this is pretty hard to follow as is. Enter AlphaGeometry! Here’s the JGEX setup for the problem:

a b c = triangle a b c; m = free m; g = on_circle g a b, on_line g b c; h = mirror h b a; i = on_line i b m, on_circle i h g; j = mirror j m i; k = reflect k j h i; e = on_line e k m, on_line e a b; d = foot d e b c ? cong e m e d

And here’s what AlphaGeometry proved:

==========================
 * From theorem premises:
A B C D E F G H I J K : Points
AE = AB [00]
E,B,C are collinear [01]
AB = AF [02]
B,A,F are collinear [03]
B,D,G are collinear [04]
FG = FE [05]
GD = GH [06]
H,D,G are collinear [07]
GH = GI [08]
FH = FI [09]
J,B,A are collinear [10]
J,D,I are collinear [11]
JK ⟂ BC [12]
K,B,C are collinear [13]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AE = AB [00] & AB = AF [02] ⇒  A is the circumcenter of \Delta FEB [14]
002. A is the circumcenter of \Delta FEB [14] & B,A,F are collinear [03] ⇒  EB ⟂ FE [15]
003. EB ⟂ FE [15] & JK ⟂ BC [12] & E,B,C are collinear [01] ⇒  FE ∥ JK [16]
004. J,B,A are collinear [10] & B,A,F are collinear [03] ⇒  J,B,F are collinear [17]
005. E,B,C are collinear [01] & K,B,C are collinear [13] ⇒  K,B,E are collinear [18]
006. EF ∥ JK [16] & B,J,F are collinear [17] & B,K,E are collinear [18] ⇒  JB:BF = KJ:EF [19]
007. GH = GI [08] & FH = FI [09] ⇒  HI ⟂ GF [20]
008. GH = GI [08] & GD = GH [06] ⇒  G is the circumcenter of \Delta HID [21]
009. G is the circumcenter of \Delta HID [21] & G,H,D are collinear [07] ⇒  HI ⟂ DI [22]
010. J,D,I are collinear [11] & HI ⟂ GF [20] & HI ⟂ DI [22] ⇒  JD ∥ FG [23]
011. JD ∥ FG [23] & B,J,F are collinear [17] & B,D,G are collinear [04] ⇒  BJ:BF = JD:FG [24]
012. JB:BF = KJ:EF [19] & BJ:BF = JD:FG [24] & FG = FE [05] ⇒  JD:FG = KJ:FG [25]
013. FG = EF [05] ⇒  FG:EB = FG:EB [26]
014. JD:FG = KJ:FG [25] & FG:EB = FG:EB [26] ⇒  JD = KJ
==========================

Once again, AlphaGeometry found a proof without requiring any auxiliary points! The construction itself contains all the geometric relationships needed to prove correctness. So what’s the idea? First understand that AlphaGeometry re-labeled every point to be consecutive(?) letters. I understand they did this because of how the underlying LLM was trained, but couldn’t they at least fix it in the UI so the user is insulated from this implementation detail? Whatever. After looking at its proof, let me add some helpful lines so we can see which triangles are important:

With those purple lines added, the construction becomes clear: it’s a projective geometry approach using homothety centered at $B$. We start by dropping a perpendicular to $\overline{BC}$ at an arbitrary point $G$, extend it to intersect $\overline{AB}$ at $H$, then mark off an equal distance along line $BM$ to get point $I$. This creates a homothetic image of our desired configuration - a valid equidistant point for some configuration, but we need to scale it so that point $I$ lands exactly at $M$. The key insight: use similar triangles. Draw a line through $M$ parallel to $\overline{HI}$, and where it intersects $\overline{AB}$ gives us the correct answer at $E$.