El teorema de Napoleón via SymPy

Programación

Durante el pasado periodo estival, como es tradición, me extrajeron alevosamente de la M-30. Me introdujeron en una caja metálica, me amarraron a una silla y me torturaron durante seis horas, en el transcurso de las cuales, las únicas percepciones del mundo exterior que impactaron mis sentidos fueron calor, ruido, cerros, pinos y dolores en las asentaderas. Como no había otra cosa que hacer y tenía frescos los enunciados de los problemas de la última olimpiada internacional de matemáticas —que, como recordarán los lectores del blog, tuvo cierto impacto mediático por el excelente resultado logrado en ellas por los LLMs más avanzados— , me puse con uno de ellos. Estoy muy pagado de mí mismo por el hecho de que, salvo por un par de cabos sueltos que solo pude rematar cuando conseguí lápiz, papel y silencio, dejé uno de ellos prácticamente resuelto.

Motivado por tal éxito, me entretuve después con algunos de los problemas que plantea V. I. Arnold para niños de 5 a 15 años. Uno de ellos, el 22, consiste en probar el conocido como problema de Napoleón:

Se construyen triángulos equiláteros en el exterior de los lados AB, BC y CA de un triángulo ABC. Probar que sus centros forman un triángulo equilátero.

Aquí está la interpretación artística que hizo Claude del enunciado:

Teorema de Napoleón

Fracasé vergonzosamente al intentar probarlo. Pero me acordé de Descartes y algunas discusiones acerca de la industrialización de la solución de ese tipo de problemas mediante la asignación de coordenadas a puntos, resolver ecuaciones, etc. y prescindiendo del papel, de la regla, del compás y del lapicero. Y, por supuesto, la posibilidad de usar ordenadores para organizar el caos de símbolos que aparecen al desarrollar las expresiones obtenidas.

Así que escribí (con la ayuda de Claude) mi primer programa usando SymPy, que es, una vez adecentado, este:

from sympy import *
from sympy.geometry import Point

a0, a1, b0, b1, c0, c1 = symbols('a0 a1 b0 b1 c0 c1', real=True)

A = Point(a0, a1)
B = Point(b0, b1)
C = Point(c0, c1)

def perpendicular_vector_ccw(vector):
    return [-vector[1], vector[0]]

def add_vector_to_point(point, vector):
    new_x = point.x + vector[0]
    new_y = point.y + vector[1]
    return Point(new_x, new_y)

def attached_triangle_barycenter(A, B):
    vector = [B.x - A.x, B.y - A.y]
    vector_perpendicular = perpendicular_vector_ccw(vector)
    C = add_vector_to_point(A, [1/2 * x for x in vector])
    C = add_vector_to_point(C, [sqrt(3)/6 * x for x in vector_perpendicular])
    return C

def distance_squared(p1, p2):
    return sum((a - b)**2 for a, b in zip(p1, p2))

bAB = attached_triangle_barycenter(A, B)
bBC = attached_triangle_barycenter(B, C)
bCA = attached_triangle_barycenter(C, A)

my_dist = distance_squared(bAB, bBC) - distance_squared(bAB, bCA)
simplify(my_dist)

Como da cero, QED.

Luego se me ocurrió la idea de que podía resolverlo también usando números complejos:

from sympy import symbols, exp, I, simplify, expand, pi, re, im, nsimplify

# 60 degree rotation
ω = exp(I*pi/3)

A, B, C = symbols('A B C', complex=True)

# Third vertices
P = B + (C - B) * ω
Q = C + (A - C) * ω
R = A + (B - A) * ω

# Centroids
G1 = (B + C + P)/3
G2 = (C + A + Q)/3
G3 = (A + B + R)/3

Para comprobar que tres complejos $z_1, z_2, z_3$ conforman un triángulo equilátero, basta comprobar que $z_1^2 + z_2^2 + z_3^2 = 0$, así que:

nsimplify(expand((G1 - G2)**2 + (G2 - G3)**2+ (G3 - G1)**2))

Pero la expresión resultante es

$$\frac{2 A^{2}}{3} - \frac{2 A^{2} e^{\frac{i \pi}{3}}}{3} + \frac{2 A^{2} e^{\frac{2 i \pi}{3}}}{3} - \frac{2 A B}{3} - \frac{2 A B e^{\frac{2 i \pi}{3}}}{3} + \frac{2 A B e^{\frac{i \pi}{3}}}{3}$$ $$ - \frac{2 A C}{3} - \frac{2 A C e^{\frac{2 i \pi}{3}}}{3} + \frac{2 A C e^{\frac{i \pi}{3}}}{3} + \frac{2 B^{2}}{3} - \frac{2 B^{2} e^{\frac{i \pi}{3}}}{3} + \frac{2 B^{2} e^{\frac{2 i \pi}{3}}}{3}$$ $$ - \frac{2 B C}{3} - \frac{2 B C e^{\frac{2 i \pi}{3}}}{3} + \frac{2 B C e^{\frac{i \pi}{3}}}{3} + \frac{2 C^{2}}{3} - \frac{2 C^{2} e^{\frac{i \pi}{3}}}{3} + \frac{2 C^{2} e^{\frac{2 i \pi}{3}}}{3}.$$

Vamos, que SymPy no parece darse cuenta de que

$$1 - \exp{\frac{i \pi}{3}} + \exp{\frac{2 \pi i}{3}} = 0,$$

que es el quid de la demostración.

En lugar de eso, uno puede hacer

simplify(expand(re((G1 - G2)**2 + (G2 - G3)**2+ (G3 - G1)**2)))

y

simplify(expand(re((G1 - G2)**2 + (G2 - G3)**2+ (G3 - G1)**2)))

que SymPy, esta vez sí, evalúa correctamente como 0.

En resumen, los sistemas de manipulación simbólica como SymPy son útiles para demostrar resultados clásicos, pero, como con casi todo, hay que tener mucho cuidado a la hora de utilizarlos.

Notas finales:

  • El código anterior demuestra no solo el teorema normal de Napoleón, sino también su versión interna: cuando los triángulos se construyen no hacia el exterior sino hacia el interior.
  • Dicen los LLMs que con otras herramientas (p.e., GeoGebra) uno no encuentra ese tipo de problemas. A saber.