自然言語で証明をするとどこかで矛盾が生じそうなんだけどそんなことはないのか?
ソフトウェアエンジニアである自分からすると、なんかもっと形式的に記述できるフォーマットに移行したほうが良いんじゃないかと思う。まあ俺は学部レベルの数学しか知らんけど。
Permalink | 記事への反応(2) | 20:08
ツイートシェア
形式的に記述する言語というのは一応存在し、coqやhollightのような証明システムがその例
ヒルベルトとかゲーデルとかの話?