https://github.com/python/cpython/commit/b86a41cbf631c959d274ad6180cf0a0ac6f6e180 commit: b86a41cbf631c959d274ad6180cf0a0ac6f6e180 branch: main author: Mark Dickinson <[email protected]> committer: StanFromIreland <[email protected]> date: 2026-07-25T16:42:44+02:00 summary:
Fix a stale link to the `math.integer.isqrt()` correctness proof (#154685) 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]
