Archive of formal proofs (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.
Explore the Archive of Formal Proofs, which is a massive collection of material built on the Isabelle Libraries and mechanically checked in Isabelle. It currently contains over 680 formalisations in a variety of areas (including Mathematics, Logic, Computer Science and Philosophy). Focus on developments of your choice according to your own interests. Describe your experiences.
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