]> git.ipfire.org Git - thirdparty/Python/cpython.git/commitdiff
Fix a stale link to the `math.integer.isqrt()` correctness proof (#154685) main
authorMark Dickinson <dickinsm@gmail.com>
Sat, 25 Jul 2026 14:42:44 +0000 (15:42 +0100)
committerGitHub <noreply@github.com>
Sat, 25 Jul 2026 14:42:44 +0000 (16:42 +0200)
Modules/mathintegermodule.c

index 0f660d461e349f877e31fc1a4f6fe3b94ffaa4ca..6d35c825349e45145a6a5b45cea1a3cab3ec5f69 100644 (file)
@@ -180,10 +180,9 @@ that the bound `(a - 1)**2 < (n >> s) < (a + 1)**2` is maintained from one
 iteration to the next. A sketch of the proof of this is given below.
 
 In addition to the proof sketch, a formal, computer-verified proof
-of correctness (using Lean) of an equivalent recursive algorithm can be found
-here:
+of correctness (using Lean) of the algorithm can be found here:
 
-    https://github.com/mdickinson/snippets/blob/master/proofs/isqrt/src/isqrt.lean
+    https://github.com/mdickinson/snippets/tree/41ce2d256fef06fb32f24fe7014cfa95173ac5e0/proofs/isqrt
 
 
 Here's Python code equivalent to the C implementation below: