Incorporating a database of graphs into a proof assistant

DOI10.1007/978-3-031-66997-2_9MaRDI QIDQ6648164

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

Publication date: 4 December 2024

zbMATH Keywords

graph theoryproof assistantsmathematical databasesformally verified mathematics

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Certifying algorithms
• A Skeptic's approach to combining HOL and Maple
• House of graphs 2.0: a database of interesting graphs and more
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• A bi-directional extensible interface between Lean and Mathematica
• Graph Theory
• Integrating a SAT solver with an LCF-style theorem prover
• The Lean Theorem Prover (System Description)
• Reducibility Among Combinatorial Problems
• Trustworthy Graph Algorithms (Invited Talk)
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• An extensible user interface for Lean 4

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)