Windmills of the minds: an algorithm for Fermat's Two Squares Theorem
summary
Formalised in HOL, the method turns Ségier’s parity argument on involutions into a concrete loop: represent n = x^2 + 4yz as windmill patterns, alternate the flip involution (swap y and z) and the mind involution (three simple cases: add, subtract, double) starting from a known non-Ségier fixed windmill, and stop when a fixed point x,y,y appears giving n = x^2 + y^2. Code has a termination proof, runs quickly for small n but is exponential in the worst case (minutes for ~11‑digit inputs).
AI-written summary · about