I am new to lean but am interested in proving correctness of graph algorithms. Is there a repository/website that talks about a proof using lean of Dijkstra's shortest path algorithm, for example?
2
-
$\begingroup$ Perhaps Kementzey's Bachelor of Science thesis is a good place to start, regarding graph representation and search. See also this closely related Question. $\endgroup$– hardmathSep 16 at 4:54
-
$\begingroup$ Sec. 4.2 of the above thesis describes shortest path finding by Dijkstra's algorithm. $\endgroup$– hardmathSep 16 at 16:00
Add a comment
|