Flyspeck I: Tame Graphs

DOI10.1007/11814771_4MaRDI QIDQ3613398zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow, Gertrud Bauer, Paula Schultz

Publication date 12 March 2009

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11814771_4

Mathematics Subject Classification ID

Packing and covering in (n) dimensions (aspects of discrete geometry) (52C17)

Recommendations

• Verified efficient enumeration of plane graphs modulo isomorphism
• Sphere packings. VI: Tame graphs and linear programs
• scientific article; zbMATH DE number 2209729
• A formal proof of the Kepler conjecture
• Flyspecking Flyspeck

Cited in

(15)

• Introduction to ``Milestones in interactive theorem proving
• A graph library for Isabelle
• Graph theory in Coq: minors, treewidth, and isomorphisms
• Flyspeck II: The basic linear programs
• Formalizing Frankl's conjecture: FC-families
• A compiled implementation of normalisation by evaluation
• Verified efficient enumeration of plane graphs modulo isomorphism
• The Isabelle Framework
• A Compiled Implementation of Normalization by Evaluation
• The dodecahedral conjecture
• Tame Graphs
• Computational logic: its origins and applications
• Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
• A formal proof of the Kepler conjecture
• A revision of the proof of the Kepler conjecture

Describes a project that uses

Uses Software

• Isabelle/HOL
• Flyspeck

This page was built for publication: Flyspeck I: Tame Graphs

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