kepler98

swMATH23625MaRDI QIDQ35396

No author found.

Source code repository: https://github.com/flyspeck/kepler98

Described by source

• A formulation of the Kepler conjecture
• A proof of the Kepler conjecture
• The Kepler Conjecture

Related Items (only showing first 100 items - show all)

Densest geodesic ball packings to \({\mathbf S^2 \times \mathbf R}\) space groups generated by screw motions ⋮ MizAR 40 for Mizar 40 ⋮ Guaranteed deterministic approach to superhedging: sensitivity of solutions of the Bellman-Isaacs equations and numerical methods ⋮ Automatic generation of statistical volume elements using multibody dynamics and an erosion-based homogenization method ⋮ Rotation invariant patterns for a nonlinear Laplace-Beltrami equation: a Taylor-Chebyshev series approach ⋮ An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps ⋮ Busy beaver machines and the observant otter heuristic (or how to tame dreadful dragons) ⋮ The local optimality of the double lattice packing ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Floating-point arithmetic on the test bench. How are verified numerical solutions calculated? ⋮ Hyperuniform states of matter ⋮ A peculiarly cerebroid convex zygo-dodecahedron is an axiomatically balanced ``House of Blues: the Circle of Fifths to the circle of Willis to cadherin cadenzas ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ Solution of the propeller conjecture in \(\mathbb R^3\) ⋮ Approximation on the Voronoi cells of the \(A_d\) lattice ⋮ Quasicrystals: the view from Stockholm ⋮ Optimal recovery of isotropic classes of twice-differentiable multivariate functions ⋮ The set of packing and covering densities of convex disks ⋮ Sphere packing bounds via spherical codes ⋮ A note on Schwartz functions and modular forms ⋮ The 3-ball is a local pessimum for packing ⋮ Computer-aided proof of Erdős discrepancy properties ⋮ A formally verified proof of the central limit theorem ⋮ The HOL Light theory of Euclidean space ⋮ ATP and presentation service for Mizar formalizations ⋮ Packing congruent hyperspheres into a hypersphere ⋮ Computer-assisted proof of performance ratios for the differencing method ⋮ On a computer-aided approach to the computation of Abelian integrals ⋮ On a generalization of Craig lattices ⋮ Contact numbers for congruent sphere packings in Euclidean 3-space ⋮ Perfect, strongly eutactic lattices are periodic extreme ⋮ Upper bound on the packing density of regular tetrahedra and octahedra ⋮ A candidate for the densest packing with equal balls in Thurston geometries ⋮ Automated theorem provers: a practical tool for the working mathematician? ⋮ Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials ⋮ Polynomial-sized topological approximations using the permutahedron ⋮ Face-centered cubic crystallization of atomistic configurations ⋮ Retrieving geometric information from images: the case of hand-drawn diagrams ⋮ An introduction to mechanized reasoning ⋮ Towards a new epistemology of mathematics ⋮ Asymptotic optimality of the triangular lattice for a class of optimal location problems ⋮ Globally optimized packings of non-uniform size spheres in \(\mathbb {R}^{d}\): a computational study ⋮ Optimality of the triangular lattice for a particle system with Wasserstein interaction ⋮ On packing \(\mathbb R^3\) with thin tori ⋮ A dense packing of regular tetrahedra ⋮ Automorphisms of modular lattices ⋮ Principal component analysis of persistent homology rank functions with case studies of spatial point patterns, sphere packing and colloids ⋮ Optimal \(N\)-point configurations on the sphere: ``magic numbers and Smale's 7th problem ⋮ The Besicovitch covering lemma and maximal functions ⋮ Long shortest vectors in low dimensional lattices ⋮ Pessimal packing shapes ⋮ Improved sphere packing lower bounds from Hurwitz lattices ⋮ Formalizing a fragment of combinatorics on words ⋮ Maximum packing densities of basic 3D objects ⋮ A revision of the proof of the Kepler conjecture ⋮ Packing twelve spherical caps to maximize tangencies ⋮ Foreword to the special focus on formal proofs for mathematics and computer science ⋮ Single-sized spheres on surfaces (S4) ⋮ Floating-point arithmetic in the Coq system ⋮ Crystallization to the square lattice for a two-body potential ⋮ Spontaneous periodic orbits in the Navier-Stokes flow ⋮ Compact packings of space with two sizes of spheres ⋮ Computing spectral measures and spectral types ⋮ Towards a proof of the 24-cell conjecture ⋮ From LCF to Isabelle/HOL ⋮ Machine learning guidance for connection tableaux ⋮ Locally optimal 2-periodic sphere packings ⋮ Optimal and non-optimal lattices for non-completely monotone interaction potentials ⋮ Verification of dynamic bisimulation theorems in Coq ⋮ Price-and-verify: a new algorithm for recursive circle packing using Dantzig-Wolfe decomposition ⋮ Historical overview of the Kepler conjecture ⋮ Sphere packings. III: Extremal cases ⋮ Sphere packings. IV: Detailed bounds ⋮ Sphere packings. VI: Tame graphs and linear programs ⋮ On percolation of two-dimensional hard disks ⋮ Stochastic protein folding simulation in the three-dimensional HP-model ⋮ Upper bounds on packing density for circular cylinders with high aspect ratio ⋮ Compact packings of the plane with three sizes of discs ⋮ Packings by translation balls in \({\widetilde{{\mathrm {SL}}_2(\mathbb{R})}}\) ⋮ Three-dimensional random Voronoi tessellations: from cubic crystal lattices to Poisson point processes ⋮ The hexagonal parquet tiling: \(k\)-isohedral monotiles with arbitrarily large \(k\). ⋮ Phase field approach to optimal packing problems and related Cheeger clusters ⋮ Experiences from exporting major proof assistant libraries ⋮ Limit theory of combinatorial optimization for random geometric graphs ⋮ A survey on spherical designs and algebraic combinatorics on spheres ⋮ Proof assistants: history, ideas and future ⋮ Global dynamics in nonconservative nonlinear Schrödinger equations ⋮ Techniques and results on approximation algorithms for packing circles ⋮ Density of binary disc packings: playing with stoichiometry ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL ⋮ Bayesian ranking for strategy scheduling in automated theorem provers ⋮ Density of binary disc packings: the nine compact packings ⋮ The future of logic: foundation-independence ⋮ Algorithm 1021: SPEX Left LU, Exactly Solving Sparse Linear Systems via a Sparse Left-looking Integer-preserving LU Factorization ⋮ A proof system for graph (non)-isomorphism verification ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A certificate-based approach to formally verified approximations

This page was built for software: kepler98