What are some useful and reliable resources for a mathematician interested in learning Isabelle/HOL? Could be online (websites) or physical (books).
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
0
Once you installed Isabelle (following these instructions), you will have all the materials listed on the tag isabelle as a local copy. Definitely go through this one for a good (field agnostic) introduction:
(you won't need to go through the whole document)
Once you are familiar with its syntax, the most common tactics and Isar you will find it most helpful to read actual code. You will find good examples by pressing Ctrl and clicking on types or constants. (as an exercise, you could click on set which leads you to HOL-Set)
Similarly, you can find other good examples in HOL-Examples.
Another most useful resource for proofs is the AFP where you will find proofs of all sorts. Many of the theories there will come with an actual paper (not just the LaTeX generated by Isabelle).
Just now, I also found this resource: Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started which shows some very beautiful Isar proofs and could be useful (I only skimmed it).
It also has some good references that are worth to track down, for example Larry Paulson's formalization(s) of Gödel's Incompleteness theorem (arxiv) one of which makes use of Isabelle/HOL's Nominal 2 framework (there is also a less powerful version shipped with Isabelle which can be found here).
