Conjecture de Kepler

La conjecture de Kepler est une ancienne conjecture (démontrée en 1998 et certifiée en 2014) formulée par le physicien, astronome et mathématicien Johannes Kepler en 1611. Cette conjecture énonce que, pour un empilement de sphères égales, en espace libre, la densité maximale est atteinte pour un empilement compact de plans compacts. Cette densité d vaut environ 74 % :

$d={\frac {\pi }{3{\sqrt {2}}}}\simeq 0{,}740\,48$.

Dans un plan compact chaque sphère est au contact de six autres. Dans l'empilement compact de deux plans compacts chaque sphère du plan supérieur est posée dans le creux formé par trois sphères du plan inférieur en contact deux à deux. Si un plan compact est noté A, les autres plans compacts peuvent être de type A, B ou C selon leur décalage horizontal par rapport au plan A. L'empilement compact est réalisé par l'empilement de plans A, B ou C de telle sorte que deux plans successifs ne soient pas du même type : ABABAB… (empilement hc, pour hexagonal compact), ABCABCABC… (empilement cfc, pour cubique à faces centrées) mais aussi ABCBABCBABCB… et n'importe quel autre succession vérifiant la condition ci-dessus, même non périodique.

László Fejes Tóth démontre en 1953 que la conjecture de Kepler pouvait être réduite à un problème à un nombre fini de paramètres.

Empilement compact de 35 sphères.

Preuve par ordinateur

En 1998, Thomas Hales a annoncé avoir démontré cette conjecture. Il réduit celle-ci à un nombre fini, mais élevé, de vérifications, qui ont été effectuées à l'aide de calculs par ordinateur. Les mathématiciens chargés de valider l'article de Hales ont affirmé être « certains à 99 % » que cette démonstration est valide. Ils y ont consacré beaucoup plus de temps que pour un article habituel de mathématiques, et la publication de l'article de Hales sur le sujet a été acceptée, ce qui indique une confiance certaine dans sa correction. Cependant le fait que de nombreux cas soient vérifiés à l'aide de calcul par ordinateur, et de façon liée, la compréhension réduite des principes généraux qui gouvernent la preuve, font que le doute subsiste qu'une erreur de détail qui n'a pas été repérée puisse affecter l'ensemble de la démonstration (contrairement à une démonstration mathématique plus usuelle quand elle est soigneusement relue, même si elle est très complexe comme celle du théorème de Fermat-Wiles).

Pour cette raison, Hales a lancé le projet Flyspeck, visant à établir une preuve formelle de son théorème, qui puisse être validée à l'aide d'un assistant de preuve sur ordinateur, capable de vérifier que les étapes de la démonstration sont logiquement valides. Ce projet réunit des informaticiens et mathématiciens de plusieurs laboratoires.

En 2009, le prix Fulkerson a été attribué à Hales (et conjointement à Samuel P. Ferguson, responsable des aspects calculatoires) pour cette démonstration, qui, bien que non encore validée par Flyspeck sous sa forme initiale, était considérée par la communauté mathématique comme complète. Celle-ci est désormais validée et un rapport sur ArXiv, signé par 22 auteurs, a été publié en 2015.

Problème voisin

Le problème posé par Kepler se rapproche d'une autre question, surgie en 1690 d'une polémique entre Newton et Gregory : combien de sphères unités peut-on disposer autour d'une sphère centrale de même rayon ? Il est possible d'en disposer 12, mais la question est de savoir s'il est possible d'en disposer 13. Une réponse négative a été apportée en 1953 par Kurt Schütte et Bartel Leendert van der Waerden.

Notes et références

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Kepler conjecture » (voir la liste des auteurs)

, dont les références étaient :

• (en) Tomaso Aste et Denis Weaire (en), The Pursuit of Perfect Packing, Institute of Physics Publishing, 2000 (ISBN 978-0-7503-0647-8)
• (en) Thomas C. Hales, « A Proof of the Kepler Conjecture », Ann. of Math., vol. 162, 2005, p. 1065-1185 [lire en ligne]
• (en) Thomas C. Hales, « Cannonballs and honeycombs », Notices Amer. Math. Soc., vol. 47, n^o  4, p. 440-449, [lire en ligne]
  « An elementary exposition of the proof of the Kepler conjecture. »
• (en) George G. Szpiro (de), Kepler's Conjecture, John Wiley & Sons, 2003 (ISBN 978-0-471-08601-7)
• (en) Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller: A formal proof of the Kepler conjecture. CoRR abs/1501.02155 (2015)

Annexes

Articles connexes

• Conjecture d'empilement d'Ulam (en)
• Conjecture de Hadwiger (géométrie combinatoire)Conjecture de Hadwiger (géométrie combinatoire)
• Empilement compact

Liens externes

• (en) Page personnelle de Thomas Hales
• (en) Revue de la démonstration de Hales
• (en) Article dans American Scientist - Dana Mackenzie
• (en) Site web du projet Flyspeck, dont le but (atteint) était d'établir une preuve formelle de la conjecture de Kepler.
• (en) Exemple concret de la conjecture de Kepler