私は今はもうP2P関連やるのは辞めちゃって
数学寄りのところにいます。
>>201 >>203 でCoqの名前が挙がってますが、
まあその辺です。
定理証明の分野は広く浅く勉強したことがあるので
ある程度はお教えできることもあるかもしれません。
実はこのスレにはリーマン予想を解決しようとしているという噂を聞いてやってきました。
私は今数理論理学から公理的集合論までの数学の基礎を
コンピュータ上で構築する試みを行っています。
Coqやその他定理証明支援系の二番煎じと言えばそうなのですが、
私は専門家向けじゃなく一般人にも分かりやすいシステムを作れないか
というところを主眼に置いています。