Mizarとか
調べてみたら、ジョルダン曲線定理のmechanical proofに絡んだ人じゃないですか。要するに、コンピュータでチェックされていない証明は認めないという方針のようです。
ジョルダン曲線定理のウィキ先生による解説はこちら。
Jordan curve theorem - Wikipedia, the free encyclopedia
ジョルダン曲線定理 - Wikipedia
英語の方ではMizarによる証明にも触れていますね。
それに関する中村先生の言葉はこちら。Adam Grabowskiの文章も下の方に。
http://e-learn.mine.nu/mizar/jordancurve.htm
コンピュータが検証できる証明を与える、というのは意味があることだと思うのですが、Oswald Veblenの証明を貶めるようなことを言うのはどうかと。実名も出さずに書いているページにこれ以上のことを書くのは控えますが。
しかし、Mizarの中でstationarityとかMahloとかもすでに定義されているようですし、集合論に対する理解もプロジェクト全体としてはトンデモではないようなのですが。うーむ。
誰か、CHの独立性をMizar(でもIsabelleでもなんでも)で証明して、中村先生を説得してくださいませんか？(他力本願)
