Graham’s Scan algorithm is a widely-used method to compute convex hulls. This paper presents its formal verification using the Rocq Proof Assistant, building upon the geometric framework outlined in Knuth’s work. We adopt Knuth’s proof strategy, decompose correctness proof into local geometric properties, and manually prove equivalent representations for crucial convex hull properties. To address degenerate cases like collinearity, which often complicate manual proofs, we introduce a novel proof-automation method by Large Language Models (LLMs), significantly reducing manual effort.