@article{10_1017_fmp_2017_1, author = {THOMAS HALES and MARK ADAMS and GERTRUD BAUER and TAT DAT DANG and JOHN HARRISON and LE TRUONG HOANG and CEZARY KALISZYK and VICTOR MAGRON and SEAN MCLAUGHLIN and TAT~THANG NGUYEN and QUANG TRUONG NGUYEN and TOBIAS NIPKOW and STEVEN OBUA and JOSEPH PLESO and JASON RUTE and ALEXEY SOLOVYEV and THI HOAI AN TA and NAM TRUNG TRAN and THI DIEP TRIEU and JOSEF URBAN and KY VU and ROLAND ZUMKELLER}, title = {A {FORMAL} {PROOF} {OF} {THE} {KEPLER} {CONJECTURE}}, journal = {Forum of Mathematics, Pi}, publisher = {mathdoc}, volume = {5}, year = {2017}, doi = {10.1017/fmp.2017.1}, language = {en}, url = {http://geodesic.mathdoc.fr/articles/10.1017/fmp.2017.1/} }