There was an error while loading. Please reload this page.
math.integer.isqrt()
1 parent 587d0d1 commit b86a41cCopy full SHA for b86a41c
1 file changed
Modules/mathintegermodule.c
@@ -180,10 +180,9 @@ that the bound `(a - 1)**2 < (n >> s) < (a + 1)**2` is maintained from one
180
iteration to the next. A sketch of the proof of this is given below.
181
182
In addition to the proof sketch, a formal, computer-verified proof
183
-of correctness (using Lean) of an equivalent recursive algorithm can be found
184
-here:
+of correctness (using Lean) of the algorithm can be found here:
185
186
- https://github.com/mdickinson/snippets/blob/master/proofs/isqrt/src/isqrt.lean
+ https://github.com/mdickinson/snippets/tree/41ce2d256fef06fb32f24fe7014cfa95173ac5e0/proofs/isqrt
187
188
189
Here's Python code equivalent to the C implementation below:
0 commit comments