Formal proof で証明出来たものが数学の定理であると定義するのは良いんだけど、誰も実際それで証明してないという大問題がある