 Euclid’s recipe is formal, and we can analyze it with formal means. The correctness of Euclid’s algorithm follows from the insight that if you have two numbers \(A\) and \(B\) with \(A\) larger than \(B\), and you replace \(A\) by \(A - B\), then the set of common divisors of the number pair does not change.