A FORMAL PROOF OF THE KEPLER CONJECTURE (Q5280247): Difference between revisions

@@ Property / cites work @@
+Flyspecking Flyspeck
@@ Property / cites work: Flyspecking Flyspeck / rank @@
+Normal rank
@@ Property / cites work @@
+Flyspeck I: Tame Graphs
@@ Property / cites work: Flyspeck I: Tame Graphs / rank @@
+Normal rank
@@ Property / cites work @@
+Q5824053
@@ Property / cites work: Q5824053 / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Developments in Formal Proofs
@@ Property / cites work: Developments in Formal Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+A proof of the Kepler conjecture
@@ Property / cites work: A proof of the Kepler conjecture / rank @@
+Normal rank
@@ Property / cites work @@
+Q2892718
@@ Property / cites work: Q2892718 / rank @@
+Normal rank
@@ Property / cites work @@
+A formulation of the Kepler conjecture
@@ Property / cites work: A formulation of the Kepler conjecture / rank @@
+Normal rank
@@ Property / cites work @@
+A revision of the proof of the Kepler conjecture
@@ Property / cites work: A revision of the proof of the Kepler conjecture / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Self-verification of HOL Light
@@ Property / cites work: Towards Self-verification of HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Without Loss of Generality
@@ Property / cites work: Without Loss of Generality / rank @@
+Normal rank
@@ Property / cites work @@
+HOL Light: An Overview
@@ Property / cites work: HOL Light: An Overview / rank @@
+Normal rank
@@ Property / cites work @@
+Scalable LCF-Style Proof Translation
@@ Property / cites work: Scalable LCF-Style Proof Translation / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+Learning-assisted theorem proving with millions of lemmas
+Normal rank
@@ Property / cites work @@
+HOL with Definitions: Semantics, Soundness, and a Verified Implementation
+Normal rank
@@ Property / cites work @@
+Formal certification of a compiler back-end or
@@ Property / cites work: Formal certification of a compiler back-end or / rank @@
+Normal rank
@@ Property / cites work @@
+Study of the Kepler's conjecture: the problem of the closest packing
+Normal rank
@@ Property / cites work @@
+An Interpretation of Isabelle/HOL in HOL Light
@@ Property / cites work: An Interpretation of Isabelle/HOL in HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Introduction to Interval Analysis
@@ Property / cites work: Introduction to Interval Analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Flyspeck II: The basic linear programs
@@ Property / cites work: Flyspeck II: The basic linear programs / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient Formal Verification of Bounds of Linear Programs
+Normal rank
@@ Property / cites work @@
+Formal Mathematics on Display: A Wiki for Flyspeck
+Normal rank