Prims_Algorithm_produces_MST

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algorithmsgraph-theoryproofwiki

Prim's Algorithm always produces a minimum spanning tree.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Prims_Algorithm_produces_MST (n : ℕ) (hn : n ≥ 1) (prim_weight mst_weight : ℝ) (h : prim_weight = mst_weight) : prim_weight = mst_weight := by sorry

Source

https://proofwiki.org/wiki/Prim's_Algorithm_produces_Minimum_Spanning_Tree

View graph