Tracking: Hopf–Rinow theorem

[AxelDlv00]

Umbrella / tracking issue for the Hopf–Rinow milestone.

Equivalence of geodesic and metric completeness, existence of minimizing geodesics, and the Heine–Borel property for connected Riemannian manifolds.

• Open sub-issues for individual lemmas/defs and link them here.
• Claim a piece via assignee + In Progress.

Sources: see the book: labels.

[alreadydone]

The LeanEval version of Hopf–Rinow was solved by @hanwenzhu with Seed Prover (ByteDance) on Jul 26, 2026
Smooth and topological Poincare conjecture are yet to be solved :)

[AxelDlv00]

The LeanEval version of Hopf–Rinow was solved by @hanwenzhu with Seed Prover (ByteDance) on Jul 26, 2026 Smooth and topological Poincare conjecture are yet to be solved :)

Thank you for noticing. I can't find his lean code though, it seems to be closed-source. Moreover the statement in Do Carmo seems a bit stronger.
I want to mention by the way that Hopf-rinow is already formalized here (In three versions : Do Carmo, Peterson and Lee), but I intend to close the issue once it has been human reviewed, the review is almost finished.

[alreadydone]

Yeah, my intention was to notify you and tag Thomas Zhu to see if he's willing to share the solution with you, but since you in fact already formalized Hopf Rinow (is it a cleanup of MathNetwork/OpenGA#112?) this point is probably moot. The submission repo in leanprover/lean-eval-submissions#886 is indeed private, though there's a recent submission "Humanifa + GPT 5.6 sol" solving 130 LeanEval problems (ranked 2nd now) that you can find on GitHub. I've found some recent formalization by Fable to be of high quality, and GPT 5.6 is probably of the same class.

[AxelDlv00]

Yes, I initially did the submission on MathNetwork/OpenGA#112, but here the proof has been changed a bit, for instance because the definition of exponential map was not general enough. Moreover the lean version here is more recent (4.32).