Kepler Conjecture settled by computer-aided proof

[Jack Campin]

https://www.sciencedaily.com/releases/2017/06/170616102155.htm

-----------------------------------------------------------------------------
e m a i l : j a c k @ c a m p i n . m e . u k
Jack Campin, 11 Third Street, Newtongrange, Midlothian EH22 4PU, Scotland
mobile [phone] <http://www.campin.me.uk> Twitter: JackCampin

[Peter Percival]

Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm

Didn't Flyspeck prove it years ago (not many years, maybe three or four)?

[Richard Tobin]

Post by Peter Percival

Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm

Didn't Flyspeck prove it years ago (not many years, maybe three or four)?

Looks like the paper has just been published - it says "Received 21
November 2014; accepted 9 December 2016".

https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC

-- Richard

[David Bernier]

Post by Richard Tobin

Post by Peter Percival

Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm

Didn't Flyspeck prove it years ago (not many years, maybe three or four)?

Looks like the paper has just been published - it says "Received 21
November 2014; accepted 9 December 2016".
https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC
-- Richard

I've been reading on Wikipedia about the face-centered cubic or FCC
lattice arrangement,

a ball on one layer (say the second layer from the bottom) touches
4 balls from the first layer, 4 balls from the second layer, and
4 balls from the third layer:

<
https://en.wikipedia.org/wiki/Close-packing_of_equal_spheres#FCC_and_HCP_Lattices
referrning to the graphic:
fcc arrangement .

Anyway, my question is:

are the fcc-lattice packing and the HCP or hcp-lattice packing isometric?

Thanks,

David

[David Bernier]

Post by David Bernier

Post by Richard Tobin

Post by Peter Percival

Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm

Didn't Flyspeck prove it years ago (not many years, maybe three or four)?

Looks like the paper has just been published - it says "Received 21
November 2014; accepted 9 December 2016".
https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC
-- Richard

I've been reading on Wikipedia about the face-centered cubic or FCC
lattice arrangement,
a ball on one layer (say the second layer from the bottom) touches
4 balls from the first layer, 4 balls from the second layer, and
<
https://en.wikipedia.org/wiki/Close-packing_of_equal_spheres#FCC_and_HCP_Lattices
fcc arrangement .
are the fcc-lattice packing and the HCP or hcp-lattice packing isometric?
Thanks,
David

No. I don't think so ...

In the FCC-lattice, the centers of the twelve spheres in contact with a
given sphere form the vertices of a cuboctahedron.

In the HCP-lattice, the centers of the twelve spheres in contact with
a given sphere form the vertices of triangular orthobicupola.

The triangular orthobicupola and the cuboctahedron (also known
as the triangular gyrobicupola) don't have the same shape:

<
https://en.wikipedia.org/wiki/Triangular_orthobicupola#Relation_to_cuboctahedra

Post by David Bernier
.

David Bernier

[Dan Christensen]

Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm

An important proof is formalized -- by using a computer, I presume -- and verified not my human referees, but by another computer. Interesting.


Dan

[Dan Christensen]

Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm

An important proof is formalized -- by using a computer, I presume -- and verified not by human referees, but by another computer. Interesting.


Dan

[Thomas Plehn]

Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm
-----------------------------------------------------------------------------
Jack Campin, 11 Third Street, Newtongrange, Midlothian EH22 4PU, Scotland
mobile [phone] <http://www.campin.me.uk> Twitter: JackCampin

it seems similar to the case of the four color theorem.

but my you help me with one simple question?

are the functions:
f_x(x,y)=h+a*x+b*y+c*xy
f_y(x,y)=g+d*x+e*y+f*xy

always describing a homography for most choices of parameters
i mean only for the special case of 2d mapping of planes


and when you create a 2d polygon out of four mapped points by a homography
first interpolating the resulting coordinates on the edges and then on the horizontal line connecting them will construct the homography given by the mapping of the four points. Of course you do interpolation three times linear.

Remeber, this is all about 2d, 4 point polygons and their mapping from one plane to another over a given homography.

can you represent them linke this in most cases?

[Dan Christensen]

Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm
-----------------------------------------------------------------------------
Jack Campin, 11 Third Street, Newtongrange, Midlothian EH22 4PU, Scotland
mobile [phone] <http://www.campin.me.uk> Twitter: JackCampin

See article at arxiv.org: https://arxiv.org/pdf/1501.02155.pdf

[b***@gmail.com]

Recently there was also some new interesting application,
concerning analysis and proof assistants:

A formally verified proof of the Central Limit Theorem
Jeremy Avigad, Johannes Hölzl, Luke Serafin - last revised 1 Feb 2017
https://arxiv.org/abs/1405.7012

Post by Dan Christensen
See article at arxiv.org: https://arxiv.org/pdf/1501.02155.pdf