>>944
P2P、1から作るのですか・・・大変だと思いますよ？

＞考えてることがほぼ同じですね。数理論理学の本とか読んでた頃もありましたけど、
＞なんか、纏まってなくて好きになれないんですよ。
数理論理学は多分にメタ的ですから。
https://togetter.com/li/988472
たとえば、1階述語論理の上で実際の「普通の」数学を展開する場合、
数理論理学の文献に書いてあるような1階述語論理に対するメタ的な議論は
ほとんど無視して構わないかと。
ただ単に1階述語論理の定義だけ基盤として採用すれば良いです。

＞人間の扱っている数学は結構曖昧で
長大な証明になってくると、数学者でも100%正しいと言える人はいなくなってきます。
たとえば、有限単純群の分類定理の証明は1万5000ページ以上の規模ですが、
この証明は99.99%くらいは正しいと言われていますが、
100%正しいと言える数学者は誰もいないとも言われています。
実際、2004年に証明の完成が宣言された後にギャップが見付かっています。
https://ja.wikipedia.org/wiki/%E6%9C%89%E9%99%90%E5%8D%98%E7%B4%94%E7%BE%A4%E3%81%AE%E5%88%86%E9%A1%9E

＞神経科学と量子計算で自動定理証明できるように
私は量子計算についてはあまり詳しくないのですが、
自動定理証明という問題は計算量的にかなり難しいので
量子計算で自動定理証明が発展するかはちょっと疑問ですね。
っていうのはほとんどの数学って決定不可能（undecidable）なんですよ。
逆に、決定可能だと証明されている数学には簡単な幾何学(Tarski[1948])があるのですが、
「円の面積」のような重要な概念が記述できないという欠陥があります。
それで、もうちょっとまともな幾何学の体系を作ろうとすると今度は決定不可能になってしまうことが証明されています。
しかも、Tarski[1948]による簡単な幾何学の体系をコンピュータ上に実装して
自動定理証明しようとすると非常に非効率なことが分かっています（使い物にならないレベル）。
じゃあ、逆に効率良く自動定理証明できる幾何学の体系ってどんなものなの？という疑問に対してはWu[1977]があります。