アインシュタインの相対性理論はすんなり受け入れられたんじゃなかったっけ？
グロタンはまぁ、受け入れられるまでに時間を要したかもだけど

形式証明は今回のケースは無理でしょ
多くの周辺分野の数学者ですら読めない論文のアイデアを、形式化なんてとてもできないと思う