swMATH23625MaRDI QIDQ35396FDOQ35396
Author name not available (Why is that?)
Official website: https://github.com/flyspeck/kepler98
Source code repository: https://github.com/flyspeck/kepler98
Cited In (only showing first 100 items - show all)
- Flyspeck II: The basic linear programs
- Sphere packing and quantum gravity
- Verification of dynamic bisimulation theorems in Coq
- Combinatorics_Words
- Guaranteed deterministic approach to superhedging: sensitivity of solutions of the Bellman-Isaacs equations and numerical methods
- A formal proof of Cauchy's residue theorem
- Formalizing ordinal partition relations using Isabelle/HOL
- Retrieving geometric information from images: the case of hand-drawn diagrams
- An extremal property of the hexagonal lattice
- A proof system for graph (non)-isomorphism verification
- Towards a proof of the 24-cell conjecture
- Global dynamics in nonconservative nonlinear Schrödinger equations
- Polynomial-sized topological approximations using the permutahedron
- Locally optimal 2-periodic sphere packings
- Selected open problems in discrete geometry and optimization
- Proof checking and logic programming
- Proof checking and logic programming
- Computational discrete geometry
- A formal proof of the Kepler conjecture
- Automorphisms of modular lattices
- Formalizing a fragment of combinatorics on words
- A note on Schwartz functions and modular forms
- Algorithm 529
- On a generalization of Craig lattices
- Eigenfunctions of the Fourier transform with specified zeros
- Efficient formal verification of bounds of linear programs
- Limit theory of combinatorial optimization for random geometric graphs
- The Besicovitch covering lemma and maximal functions
- Self-similar singularity of a 1D model for the 3D axisymmetric Euler equations
- Computer-assisted proofs in PDE: a survey
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Classification of alignments between concepts of formal mathematical systems
- Study of the Kepler's conjecture: the problem of the closest packing
- High-dimensional sphere packing and the modular bootstrap
- Sphere packings. IV: Detailed bounds
- Sphere packings. VI: Tame graphs and linear programs
- What's in a theorem name?
- Approximation on the Voronoi cells of the \(A_d\) lattice
- Critical configurations of solid bodies and the Morse theory of min functions
- Hyperuniform states of matter
- Title not available (Why is that?)
- The role of the Mizar mathematical library for interactive proof development in Mizar
- On Minimal Tilings with Convex Cells Each Containing a Unit Ball
- On percolation of two-dimensional hard disks
- Efficient approximations for the online dispersion problem
- Three-dimensional random Voronoi tessellations: from cubic crystal lattices to Poisson point processes
- Iterative refinement for linear programming
- On a computer-aided approach to the computation of Abelian integrals
- Proof assistants: history, ideas and future
- Stochastic protein folding simulation in the three-dimensional HP-model
- Introduction to model checking
- ARQMath
- Checking proofs
- Dense crystalline dimer packings of regular tetrahedra
- Introduction to rigorous numerics in dynamics: General functional analytic setup and an example that forces chaos
- Automated theorem provers: a practical tool for the working mathematician?
- A dense packing of regular tetrahedra
- A revision of the proof of the Kepler conjecture
- Asymptotic optimality of the triangular lattice for a class of optimal location problems
- Single-sized spheres on surfaces (S4)
- Algebraic cycles from a computational point of view
- On the hard sphere model and sphere packings in high dimensions
- COLAMD
- Givaro
- LinBox
- MPFI
- SLEDGE
- SLEIGN2
- Isabelle/Isar
- SLEIGN
- Isar
- QSopt_ex
- Isabelle/ZF
- QSopt-Exact
- HOL Light
- C-CoRN
- Automath
- jSpin
- LCF
- CakeML
- Intsolver
- NLCertify
- symamd
- CertiCrypt
- DESUMA
- GIDDES
- SAD
- COLMOD
- ATL
- Flyspeck
- SymPol
- SPQR_RANK
- Poly/ML
- Coquelicot
- HybridSal
- Mtac
- QuickChick
- ROSCoq
- dedukti
- TCT
This page was built for software: kepler98
