# For formal proofs of graph structures and algorithms, which proof assistant should I learn?

My goal is to be able to make formal proofs for graph structures and algorithms, proving i.e. for every vertex in a directed-acyclic-graph there exists a path from a source vertex to that vertex, or i.e. proving the correctness of binary search on a sorted list.

For this, would you recommend learning Coq, Lean, Isabelle, or any others?

I recently started learning Coq, up to the point of proving basic boolean logic, working with lists via the (front :: rest) constructor, and basic induction proofs on the natural numbers. I've heard of Isabelle and Lean, I've just tried a few tutorials propositional statements in Lean. So far, it feels nothing like the informal proofs for discrete algorithms that I had to do in my college classes.

Most of the tutorials I find on the internet for Coq/Lean/Isabelle do stuff with propositional logic or number theory. I haven't gotten to the point where I would even know how to define what a vertex/edge is in Coq.

• I might write a longer answer, but the short version is: All three should be ok. There are many ways to define graphs in theorem proving (just like there are many ways to code graphs in a program). If your theorem requires a lot of fancy background, you may need to build off of existing work. Otherwise all the theorem provers should be fine for graph theory. As for binary search, any theorem prover should be able to prove this without issue. But note that lists are linked lists, so binary search wouldn’t be efficient. Lean also has arrays with efficient access. Commented Mar 16 at 17:34
• Functional Programming in Lean (lean-lang.org/functional_programming_in_lean) works up to proving merge sort in the end, which is similar to the kind of stuff you want to prove. But again, there are likely similar resources in Isabelle or Lean. Again your theorems don’t really require specialized tools, it is just a matter of learning the language well enough to prove them. Commented Mar 16 at 18:06
• "I haven't gotten to the point where I would even know how to define what a vertex/edge is in Coq." I think you could do this in multiple ways (adjacency matrices, relations, adjacency lists) with several possible implementation details. Unfortunately, I don't think we know what is the "best" way. Commented Mar 16 at 23:20
• See this related question for how to define a graph in Lean: proofassistants.stackexchange.com/questions/1698/… Commented Mar 17 at 3:20

I believe both Lean and Isabelle are good candidates for formalizing your proofs of algorithms on graphs. Here are some entry points for both assistants.

A simple natural language query using Moogle leads you to the Mathlib documentation on undirected graphs. A good introductory reading on defining mathematical structures on is the Mathematics in Lean book. If you need something more basic, you could check The Mechanics of Proof; this one actually contains some material on relations and graphs.

On the other hand, an analogous query on Isabelle's Archive of Formal Proofs returns many formalizations of graph algorithms; for instance, the fifth hit is Kruskal's Algorithm for Minimum Spanning Forest. There actually are lists by topic, the one for graphs being this one.