Beautiful formalizations in Isabelle/Naproche

DOI10.1007/978-3-030-81097-9_2zbMath1485.68290OpenAlexW3184839407MaRDI QIDQ2128789

Marcel Schütz, Peter Koepke, Anton Lorenzen, Erik Sturzenhecker, Adrian De Lon, Adrian Marti

Publication date: 22 April 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81097-9_2

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

CICM'22 system entries ⋮ The formal verification of the ctm approach to forcing

Uses Software

• Isabelle
• SAD
• ForTheL
• Naproche
• Archive Formal Proofs
• Furstenberg topology

Cites Work

• Unnamed Item
• The phenomenology of mathematical beauty
• Are these the most beautiful?
• A lattice-theoretical fixpoint theorem and its applications
• Beauty Is Not Simplicity: An Analysis of Mathematicians' Proof Appraisals
• On the Infinitude of Primes
• System for Automated Deduction (SAD): A Tool for Proof Verification
• On Correctness of Mathematical Texts from a Logical and Practical Point of View
• Premise Selection in the Naproche System
• Proofs from THE BOOK
• Furstenberg topology

This page was built for publication: Beautiful formalizations in Isabelle/Naproche