何でこういうのにpolymath使わないんだろうね
結局よくわからないがほとんど誰も証明を理解してないって話になるのか