Matematik dünyasının en zorlu problemlerinden biri olan yüksek boyutlu küre paketleme probleminin 8 ve 24 boyutlarındaki çözümleri, Gauss adlı otomatik kanıtlama aracı kullanılarak resmen doğrulandı. Bu başarı, E8 kafesinin ve Leech kafesinin kendi boyutlarında çakışmayan kürelerin mümkün olan en yoğun düzenlemelerini sağladığını kesin olarak kanıtlıyor. Bu sonuçlar, 2022 Fields Madalyası'nı kazanan Maryna Viazovska ve ekibi tarafından orijinal olarak kanıtlanmıştı. Viazovska'nın modüler formlar teorisiyle kurduğu şaşırtıcı bağlantı, 8. boyutta ve kısa süre sonra 24. boyutta problemi çözmesini sağlamıştı.
Formalizasyon projesi, Sidharth Hariharan ve Maryna Viazovska tarafından 2024'te başlatıldı. Ekip, Mathlib'de bulunmayan küre paketlemeleri, kafesler ve modüler formlar hakkında yeni tanımlar ve teoremler içeren kapsamlı bir kod tabanı geliştirdi. Gauss'un önceki bir sürümüyle modüler formlar ve temel küre paketleme teorisi hakkında çeşitli gerçekleri başarıyla kanıtladıktan sonra, projenin geri kalanını tamamlama hedefi belirlendi. Gauss, 8 boyutlu durum için kalan tüm sonuçları sadece 5 günde otomatik olarak kanıtlayarak, mevcut araçlarla altı ay süreceği tahmin edilen bir işi büyük ölçüde hızlandırdı. Ardından, 24 boyutlu durumu da iki hafta içinde orijinal makaleyi girdi olarak kullanarak otomatik olarak formalize etti. Bu, toplam küre paketleme formalizasyonunu 70 bin satırdan yaklaşık 200 bin satıra çıkardı.
Bu, 21. yüzyılda Fields Madalyası kazanan bir matematiksel sonucun ilk tam resmi doğrulamasıdır ve otomatik kanıtlama araçlarının karmaşık matematiksel problemleri çözme potansiyelini göstermektedir.