Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project

DOI10.1007/978-3-031-42753-4_1arXiv2305.14407OpenAlexW4386297941MaRDI QIDQ6118809

Lawrence Charles Paulson

Publication date: 28 February 2024

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2305.14407

zbMATH Keywords

formalisation of mathematicsIsabelleALEXANDRIA project

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Four decades of {\textsc{Mizar}}. Foreword
• From types to sets by local type definition in higher-order logic
• Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1--4, 2020. Proceedings. Part I
• A modular first formalisation of combinatorial design theory
• Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL
• The transcendence of certain infinite series
• Irrational rapidly convergent series
• Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
• A Theorem in the Partition Calculus
• Toward Mechanical Mathematics
• Introduction to Ramsey Spaces (AM-174)
• The Four Colour Theorem: Engineering of a Formal Proof
• Algebraically Closed Fields in Isabelle/HOL
• Schemes in Lean
• Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types
• Formalizing Ordinal Partition Relations Using Isabelle/HOL
• Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
• A short proof of a partition theorem for the ordinal ωω
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• A Machine-Checked Proof of the Odd Order Theorem
• On the irrationality of certain series
• Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
• Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis

This page was built for publication: Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project