Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started

DOI10.1365/s13291-020-00221-1zbMath1495.68241OpenAlexW3091930284MaRDI QIDQ2657827

Angeliki Koutsoukou-Argyraki

Publication date: 15 March 2021

Published in: Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1365/s13291-020-00221-1

zbMATH Keywords

proof assistantformalisation of mathematicsIsabelle/HOLinteractive theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Digital mathematics libraries and repositories (68V35)

Related Items (3)

Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL ⋮ Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project ⋮ On preserving the computational content of mathematical proofs: toy examples for a formalising strategy

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• kepler98
• MathOverflow
• Archive Formal Proofs
• Aristotles_Assertoric_Syllogistic
• Octonions
• Amicable Numbers
• Irrationality_J_Hancl
• Transcendence_Series_Hancl_Rucki
• Irrational_Series_Erdos_Straus
• Quaternions
• Pratt_Certificate
• FindFacts
• SErAPIS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators
• Effective asymptotic regularity for one-parameter nonexpansive semigroups
• How to write a 21\(^{\text{st}}\) century proof
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Isabelle/HOL. A proof assistant for higher-order logic
• The foundation of a generic theorem prover
• A corrected quantitative version of the Morse lemma
• A proof of the Kepler conjecture
• The transcendence of certain infinite series
• Irrational rapidly convergent series
• A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
• Proof Analysis
• Opinion: The Mechanization of Mathematics
• Computational logic: its origins and applications
• Effective Rates of Convergence for the Resolvents of Accretive Operators
• PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS
• Hammering towards QED
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• The challenge of computer mathematics
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Rational approximations to algebraic numbers
• On the irrationality of certain series

This page was built for publication: Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started