Skip to content

Fix a stale link for the math.integer.isqrt correctness proof#154685

Open
mdickinson wants to merge 3 commits into
python:mainfrom
mdickinson:fix-stale-isqrt-proof-link
Open

Fix a stale link for the math.integer.isqrt correctness proof#154685
mdickinson wants to merge 3 commits into
python:mainfrom
mdickinson:fix-stale-isqrt-proof-link

Conversation

@mdickinson

Copy link
Copy Markdown
Member

The math.integer C source contains a link to an old proof of correctness for the math.integer.isqrt algorithm. That old proof, written in the obsolete language Lean 3, no longer exists at the given URL. This PR:

  • updates the URL to point to the current proof, written in Lean 4
  • removes the "an equivalent recursive algorithm" hedge, since the Lean 4 proof directly proves correctness of the iterative form of the algorithm

I didn't create an issue for this trivial comment-only change. Let me know if you think it needs one.

@mdickinson

mdickinson commented Jul 25, 2026

Copy link
Copy Markdown
Member Author

I updated the URL to use a permalink, to reduce the likelihood of the link breaking in the future. There's a tradeoff here: Lean 4 evolves fairly rapidly, so there's a risk that the permalink version will eventually not compile. (The project locks the version of Lean 4 that it builds against, so the build won't break purely because a new version of Lean 4 with backwards-incompatible changes has been released. But there are other possible evolutionary failure modes.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant