Isabelle (Koutsoukou-Argyraki)
This topic refers to the course Automated reasoning and proof assistants for mathematics (Koutsoukou-Argyraki). Here is a description and a bibliography for addressing it.
Install Isabelle (optionally: also install the Archive of Formal Proofs, for information see this topic) and experiment with basic examples of your choice according to your interests.
USEFUL LINKS
Isabelle Webpage (includes installation instructions and a collection of user manuals)
Programming and proving in Isabelle/HOL (main user manual)
SUPPORT
Subscribe to the Isabelle Zulip Chat
Subscribe to the Isabelle Mailing List
BIBLIOGRAPHY
Machine Logic (blog by L. C. Paulson) [In particular see the posts containing instructions and simple examples for Isabelle/HOL beginners, e.g. 11 May, 4 May, 13 April, 13 October, 17 November]
F. Wiedijk, Formalising 100 theorems
A. Koutsoukou-Argyraki, Aristotle's Assertoric Syllogistic, Formal Proof Development, Archive of Formal Proofs, October 2019
A. Koutsoukou-Argyraki, What can formal systems do for mathematics? A discussion through the lens of proof assistants: some recent advances, Q&A with Jeremy Avigad, Jasmin Blanchette, Frédéric Blanqui, Kevin Buzzard, Johan Commelin, Manuel Eberl, Timothy Gowers, Peter Koepke, Assia Mahboubi, Ursula Martin, Lawrence C. Paulson. Invited contribution. To appear in: Benedikt Löwe and Deniz Sarikaya (eds), 60 Jahre DVMLG (special issue for the 60 years of the DVMLG), Series: "Tributes", vol. 48 of Tributes, College Publications, London, 2022
A. Koutsoukou-Argyraki, Formalising mathematics - in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started, in Jahresbericht der Deutscher Mathematiker-Vereinigung, 123, pp. 3-26, 2021
Bayer, J., Benzmüller, C., Buzzard, K., David, M., Lamport, L., Matiyasevich, Y., Paulson, L.C., Schleicher, D., Stock, B., Zelmanov, E.: Mathematical Proof Between Generations, arXiv (2022) https://arxiv.org/abs/2207.04779
Buzzard, K.: What is the point of computers? A question for pure mathematicians, to appear in the Proceedings of the International Congress of Mathematicians (ICM 2022) https://arxiv.org/abs/2112.11598v2