generated at
ケプラー予想
2014年にIsabelleHOL Lightの組み合わせによって形式証明された
元未解決問題



参考