ケプラー予想 - mrsekut-p

ケプラー予想

2014年にIsabelleとHOL Lightの組み合わせによって形式証明された

元未解決問題

https://ehito.hatenablog.com/entry/20111102/1320211246

https://en.wikipedia.org/wiki/HOL_Light

参考

https://ja.wikipedia.org/wiki/ケプラー予想