どんな誤りが些細なミスなのか

どんな誤りが些細なミスなのか

要点

1. ある定義や証明にある誤りが修正しやすくても、気づくのが難しいなら、そのミスは些細ではありません。
2. ある種の誤りは、証明支援系の助けを借りなければ見つけられません。

要約本文

• 昨年12月から今年4月16日までに約170時間をかけて、Lean証明支援系の標準ライブラリにある文字列定理String.splitOn_of_validを証明しました。
• この定理を証明する途中で、String.splitOn 関数の定義にあるバグを発見しました。
• このバグを修正すること自体はそれほど難しくありませんでした。該当する定義で i を i - j に置き換えるだけでよかったのです。
• だからといって、この誤りが些細なミスだったとは思いません。この定義では splitOn 関数はたいてい正しく動作しますが、特殊な場合には誤った結果を返すからです。
• Leanのような証明支援系を使っていなければ、私はこのような微妙な誤りを絶対に見つけられなかったでしょう。