## Stream: Mirror: Isabelle Users Mailing List

### Topic: [isabelle] First day with HOL/Isabelle

#### Email Gateway (Feb 21 2021 at 11:05):

From: "McCue, Brian" <brian.mccue@snhu.edu>
Can HOL/Isabelle be used with graph theory to prove whether a graph is isomorphic?

(I am a first-year math student and start classes next week. I was installing Python TensorFlow and some libraries led me to HOL/Isabelle).

Thank you for looking at my question above.

#### Email Gateway (Feb 21 2021 at 15:49):

From: "C. Diekmann" <diekmann@in.tum.de>
<trolling>I don't think that Isabelle/HOL can prove that one graph is
isomorphic, but Isabelle/HOL may be able to prove that two graphs are
isomorphic or that any graph is isomorphic to itself.</trolling>

As an example, https://www.isa-afp.org/entries/Graph_Theory.html contains
one section labeled "Isomorphisms of Digraphs".

HTH
Cornelius

#### Email Gateway (Feb 21 2021 at 18:29):

Brian,

there is a formalization of some aspects of graph theory available here:

https://www.isa-afp.org/entries/Graph_Theory.html

In particular, isomorphisms are defined for directed graphs in section
11 of the proof document (theory Digraph_Isomorphism). You can also use
it for undirected graphs by ensuring all edges are bidirectional.

Regards,
Jakub Kądziołka

#### Email Gateway (Feb 21 2021 at 20:04):

From: Thomas Sewell <tals4@cam.ac.uk>
Other people have given you some detailed/specific answers, but I think
that, since you found Isabelle by following libraries around, we should
clear up the general picture a bit. Isabelle is mostly a tool for
checking
proofs that are well understood. If you think you have an argument or
proof