Discussion:
Kepler Conjecture settled by computer-aided proof
(too old to reply)
Jack Campin
2017-06-17 14:16:06 UTC
Permalink
Raw Message
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 07895 860 060 <http://www.campin.me.uk> Twitter: JackCampin
Peter Percival
2017-06-17 14:19:52 UTC
Permalink
Raw Message
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)?
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
Richard Tobin
2017-06-17 14:29:30 UTC
Permalink
Raw Message
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
2017-06-17 16:21:32 UTC
Permalink
Raw Message
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
2017-06-17 21:01:00 UTC
Permalink
Raw Message
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
2017-06-17 14:42:08 UTC
Permalink
Raw Message
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
2017-06-17 14:44:33 UTC
Permalink
Raw Message
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
2017-06-17 16:08:47 UTC
Permalink
Raw Message
Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm
-----------------------------------------------------------------------------
Jack Campin, 11 Third Street, Newtongrange, Midlothian EH22 4PU, Scotland
mobile 07895 860 060 <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
2017-06-17 18:39:27 UTC
Permalink
Raw Message
Post by Jack Campin
https://www.sciencedaily.com/releases/2017/06/170616102155.htm
-----------------------------------------------------------------------------
Jack Campin, 11 Third Street, Newtongrange, Midlothian EH22 4PU, Scotland
mobile 07895 860 060 <http://www.campin.me.uk> Twitter: JackCampin
See article at arxiv.org: https://arxiv.org/pdf/1501.02155.pdf
b***@gmail.com
2017-06-17 19:16:10 UTC
Permalink
Raw Message
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
Loading...