謝罪するしないはともかくとして、今回のLANAの発表については一言ないとあかんやろ。
形式化できませんでしたって言ってるんだから
論文間違ってるよと指摘されてるんやから
可能性は２つ
・確かに正しく形式化されていて証明にギャップがあるというのは正しい
・そもそも形式化が間違ってる
前者なら当然論文は撤回すべきだし、後者ならじゃあどう形式化されるのか、Leanではどのように形式化されるのか、そもそもできないのか、ならどんな言語下なら形式化できるのか、そもそも形式化すできないのか
なんか言わんと
間違ってるって言われてるんやから