%0 Journal Article
%A THOMAS HALES
%A MARK ADAMS
%A GERTRUD BAUER
%A TAT DAT DANG
%A JOHN HARRISON
%A LE TRUONG HOANG
%A CEZARY KALISZYK
%A VICTOR MAGRON
%A SEAN MCLAUGHLIN
%A TAT THANG NGUYEN
%A QUANG TRUONG NGUYEN
%A TOBIAS NIPKOW
%A STEVEN OBUA
%A JOSEPH PLESO
%A JASON RUTE
%A ALEXEY SOLOVYEV
%A THI HOAI AN TA
%A NAM TRUNG TRAN
%A THI DIEP TRIEU
%A JOSEF URBAN
%A KY VU
%A ROLAND ZUMKELLER
%T A FORMAL PROOF OF THE KEPLER CONJECTURE
%J Forum of Mathematics, Pi
%D 2017
%V 5
%I mathdoc
%U http://geodesic.mathdoc.fr/articles/10.1017/fmp.2017.1/
%R 10.1017/fmp.2017.1
%G en
%F 10_1017_fmp_2017_1