定理証明器のα変換バグ

定理証明器自体の実装が正しいか、という話があったのでついでに：ある定理証明器にはα変換のバグが存在して、6年ぐらい発見されず放置されていたそうです。

まあ、実際に何か間違った定理が証明されてしまったわけではないようですが（わざと作った反例以外）。しかし、古いアーカイブの日付やスレッドの表示が壊れてるなあ…。De Bruijn indexの話で盛り上がっていますが、この頃から自分がOCaml メーリングリストを荒らしていたことは秘密です。