A Pythagorean Triple for 2025

Coding, Number Theory 3 Minutes

Happy 2025 to everyone! As one exciting update, I plan to work more on AI for math education this year, including more work in number theory. I hope to publish some updates to my number theory book with more completed chapters if all goes well.

The following puzzle was posed to me in an email by Professor Paul Buckingham. Paul has been a big inspiration to me for a while for his mentoring of me in Algebraic Number Theory, so I knew it’d be a good problem. It led to some twists and turns in number theory and computer science, so I’m sharing it below with his permission.

Problem: Show that there are pairwise coprime positive integers x,y, and z such that: x^2+y^2=z^2 and \dfrac{x}{x+y+z}=\dfrac{1}{2}-\dfrac{1}{2025}.

Solution: We must consider two cases based on whether x is odd or even. In the first case, we know that the primitive Pythagorean triple can be generated by (x,y,z) = (m^2-n^2, 2mn, m^2+n^2) where m and n are pairwise relatively prime and have opposite parity. If you’re unfamiliar with this formula, please see my notes here.

Substituting these values into the equation gives us:

\frac{x}{x+y+z} = \frac{m^2-n^2}{(m^2-n^2)+2mn+(m^2+n^2)}=\frac{(m-n)(m+n)}{2m^2+2mn}=\frac{(m-n)(m+n)}{2m(m+n)}=\frac{m-n}{2m}=\frac{1}{2}-\frac{n}{2m}

Therefore, we have that \dfrac{n}{2m}=\dfrac{1}{2025}. The only coprime positive integers that satisfy this are n=2 and m=2025. These generate the solution triplet (x,y,z)=(4100621, 8100, 4100629).

In the second case when x is even, we arrive at the equation:

\dfrac{x}{x+y+z} = \dfrac{2mn}{2m^2+2mn} = \dfrac{n}{m+n} = \dfrac{1}{2}-\dfrac{1}{2025}=\dfrac{2023}{4050}.

Therefore, we have that n=2023 and m=2027. However, this gives a non-primitive solution since n and m are the same parity (it actually gives double the solution found above).

Hence, the only primitive Pythagorean triple that satisfies this equation is (x,y,z)=\boxed{(4100621, 8100, 4100629)}.

I then shared this puzzle with the professor who got me into computer science, Dr. Richard Kelley. He was recently learning the Lean Proof Assistant and decided it’d be a fun exercise to code up the solution in Lean. Below is a screenshot of the code he wrote, showing how the proof assistant checks the math to ensure the solution is valid.

-- Code written by Richard Kelley
import Mathlib.NumberTheory.PythagoreanTriples
def x : ℤ := 4100621
def y : ℤ := 8100
def z : ℤ := 4100629

def FractionalEq (x y z : â„š) : Prop :=
( x / (x + y + z) ) = ( (1/2) - (1/2025) )

-- The coercion from ℤ to ℚ is necessary to be able to use the ring_nf tactic.
example : FractionalEq (x : â„š) (y : â„š) (z : â„š) := by
rw[x,y,z]
rw[FractionalEq]
ring_nf

example : (PythagoreanTriple x y z) ∧ (FractionalEq (x:ℚ) (y:ℚ) (z:ℚ)) := by
rw[x,y,z]
constructor
case left =>
rw[PythagoreanTriple]
simp
case right =>
rw[FractionalEq]
ring_nf

Extension of the problem:

Can a computer search to find the primitive Pythagorean triple we found to this? My suspicion is no, unless we’re able to put tight bounds on x,y,z. Since my master’s thesis used a lot of logic programming, I attempted to program it in Clingo (a language for answer set programming). Unfortunately, my code failed to return a solution in a reasonable amount of time. If anyone has suggestions for how to get a computer search to find this solution, I’d love to hear them in the comments below!


pythagoreanTriple(X,Y,Z) :- X=1..n, Y=1..X, Z=X..n, (X**2)+(Y**2)=(Z**2).
divisionCondition(X,Y,Z) :- X=1..n, Y=1..X, Z=X..n, X/(X+Y+Z) = 1/2 - 1/2025.
satisfiesTriple(X,Y,Z) :- X=1..n, Y=1..X, Z=X..n, pythagoreanTriple(X,Y,Z), divisionCondition(X,Y,Z).
#show satisfiesTriple/3.

Happy year 2025 = 45^2 = (20+25)^2 = \displaystyle \sum_{n=1}^{9}n^3 to you all.

Published by Justin

Published

Leave a Reply