У журналі пройшла наукове рецензування і опублікована стаття з формальним доказом теореми Кеплера. Формулювання теореми: серед всіх упаковок куль рівного розміру в тривимірному просторі найбільшу середню щільність має гранецентрована кубічна упаковка і упаковки, рівні їй за щільністю. Це завершує майже 20-річний пласт робіт, присвячених перевірці доказу Томаса Хейлза. Про це повідомляє блог Cambridge Core.
Гіпотеза Кеплера була сформульована на початку XVII століття, понад 400 років тому. Вона, почасти, була пов'язана з реальним практичним завданням про кращий спосіб упаковки гарматних ядер. Середньою щільністю упаковки називається частка заповненого шарами об'єму в досить великому (порівняно з розміром кулі) кубі простору. Незважаючи на гадану простоту, гіпотезу не вдавалося довести до кінця XX століття. Детальніше про цю історію можна прочитати в нашому матеріалі «Один зламав, інший втратив».
Перший доказ гіпотези Кеплера представив Томас Хейлз 1998 року. Воно включало в себе комп'ютерний перебір величезної кількості варіантів торкання куль між собою. Однак у доказі була деяка проблема, пов'язана з тим, що комп'ютери оперують цілими числами - потрібно було довести, що наближені таким чином обчислення коректно використовувати. Перевірка роботи Хейлза затягнулася до 2005 року. Рецензенти зазначили, що, швидше за все, доказ правильний, але перевірити всі приватні випадки вручну було неможливо. Тим не менш, перша версія доказу була опублікована.
Хейлз об'єднався з великою міжнародною групою математиків для того, щоб зробити доказ повним і формальним. Для цього математикам знову довелося використовувати комп'ютерні методи. Робота тривала ще близько десяти років, поки в 2014 році математики не оголосили про її завершення. У 2015 році Хейлз опублікував препринт фінальної статті - версію, не перевірену рецензентами.
Через два з половиною роки, 29 травня стаття остаточно пройшла рецензування і була опублікована в науковому журналі. Код, що «доводить» теорему Кеплера, опублікований у відкритому доступі на сервісі GitHub. Як зазначає блог Cambridge Core, це найбільший і складний доказ з усіх, які коли-небудь були підтверджені за допомогою комп'ютера.
Теорема Кеплера була сформульована для тривимірного простору, але відомі результати і для просторів вищих розмірностей. Так, завдання про упаковку куль у 8- і 24-мірних просторах була вирішена Мариною В'язовською (за це їй була присуджена премія інституту Клея). Варто зазначити, що це завдання має реальне практичне застосування - для передачі інформації. Найщільніші упаковки визначають, як слід кодувати інформацію, щоб невеликі випадкові шуми при її передачі не призводили до помилок при декодуванні.
Раніше ми повідомляли про комп'ютерний доказ, повний обсяг якого зайняв 200 терабайт. Таким чином було вирішено завдання про бульові піфагорові трійки.