1年以上取り組んで乗り越えられなかった壁が数か月で解決するはずない。
そもそも正しい証明の形式化に壁があること自体おかしい。