https://github.com/python/cpython/commit/1667a6c2acb022ecca37d3dc68b3d67ef186215e
commit: 1667a6c2acb022ecca37d3dc68b3d67ef186215e
branch: 3.15
author: Miss Islington (bot) <[email protected]>
committer: StanFromIreland <[email protected]>
date: 2026-07-25T15:17:11Z
summary:

[3.15] Fix a stale link to the `math.integer.isqrt()` correctness proof 
(GH-154685) (#154698)

(cherry picked from commit b86a41cbf631c959d274ad6180cf0a0ac6f6e180)

Co-authored-by: Mark Dickinson <[email protected]>

files:
M Modules/mathintegermodule.c

diff --git a/Modules/mathintegermodule.c b/Modules/mathintegermodule.c
index 0f660d461e349f..6d35c825349e45 100644
--- a/Modules/mathintegermodule.c
+++ b/Modules/mathintegermodule.c
@@ -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:

_______________________________________________
Python-checkins mailing list -- [email protected]
To unsubscribe send an email to [email protected]
https://mail.python.org/mailman3//lists/python-checkins.python.org
Member address: [email protected]

Reply via email to