Incorporating a database of graphs into a proof assistant

DOI10.1007/978-3-031-66997-2_9MaRDI QIDQ6648164zbMATH OpenFDO

Authors Andrej Bauer, Katja Berčič, Gauvain Devillez, Jure Taslak

Publication date 4 December 2024

Full work available at URL https://doi.org/10.1007/978-3-031-66997-2_9

zbMATH Keywords

formally verified mathematicsgraph theorymathematical databasesproof assistants

Mathematics Subject Classification ID

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

Cites work

• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• A bi-directional extensible interface between Lean and Mathematica
• A formal proof of the Kepler conjecture
• A Skeptic's approach to combining HOL and Maple
• An extensible user interface for Lean 4
• Certifying algorithms
• Graph theory
• House of graphs 2.0: a database of interesting graphs and more
• Integrating a SAT solver with an LCF-style theorem prover
• LEDA. A platform for combinatorial and geometric computing. 2-part set
• Reducibility among combinatorial problems
• The Lean theorem prover (system description)
• Trustworthy Graph Algorithms (Invited Talk)

Describes a project that uses

Uses Software

• SageMath

This page was built for publication: Incorporating a database of graphs into a proof assistant

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6648164)