From cadde2febab46d15499f9275fbc697ec129ac2f7 Mon Sep 17 00:00:00 2001 From: Mark Dickinson Date: Sat, 25 Jul 2026 10:13:12 +0100 Subject: [PATCH 1/3] Fix a stale link for the math.integer.isqrt correctness proof --- Modules/mathintegermodule.c | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Modules/mathintegermodule.c b/Modules/mathintegermodule.c index 0f660d461e349f..8bcbbd60b1b238 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/main/proofs/isqrt Here's Python code equivalent to the C implementation below: From 9f2c4196b84b9d11c6bc3669126fe3333f34d738 Mon Sep 17 00:00:00 2001 From: Mark Dickinson Date: Sat, 25 Jul 2026 10:46:46 +0100 Subject: [PATCH 2/3] Use a permalink, to reduce the risk of future staleness --- Modules/mathintegermodule.c | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Modules/mathintegermodule.c b/Modules/mathintegermodule.c index 8bcbbd60b1b238..53b1374ecac987 100644 --- a/Modules/mathintegermodule.c +++ b/Modules/mathintegermodule.c @@ -182,8 +182,7 @@ 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 the algorithm can be found here: - https://github.com/mdickinson/snippets/tree/main/proofs/isqrt - + https://github.com/mdickinson/snippets/tree/41ce2d256fef06fb32f24fe7014cfa95173ac5e0/proofs/isqrt Here's Python code equivalent to the C implementation below: From 0b874993240b458993ff148352c05806046cbdda Mon Sep 17 00:00:00 2001 From: Mark Dickinson Date: Sat, 25 Jul 2026 11:14:07 +0100 Subject: [PATCH 3/3] Restore accidentally-deleted blank line --- Modules/mathintegermodule.c | 1 + 1 file changed, 1 insertion(+) diff --git a/Modules/mathintegermodule.c b/Modules/mathintegermodule.c index 53b1374ecac987..6d35c825349e45 100644 --- a/Modules/mathintegermodule.c +++ b/Modules/mathintegermodule.c @@ -184,6 +184,7 @@ of correctness (using Lean) of the algorithm can be found here: https://github.com/mdickinson/snippets/tree/41ce2d256fef06fb32f24fe7014cfa95173ac5e0/proofs/isqrt + Here's Python code equivalent to the C implementation below: def isqrt(n):