- 1 名前：片山博文MZ ◆T6xkBnTXz7B0 転載ダメ©2ch.net mailto:sageteoff [2015/01/23(金) 01:41:03.17 ID:kQ1pk3tS]
- Coqというプログラムを使えば、計算機上で数学的な証明を厳密に行うことができます。
www.iij-ii.co.jp/lab/techdoc/coqt/
ja.wikipedia.org/wiki/Coq
使いこなすには、大学レベルの数学と論理学とプログラミングと英語の知識が必要。
さあ、試してみよう！
- 44 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/28(水) 18:52:58.11 ID:xr03hxaD]
- >>41
単純に言えば、コンピューターでできた数学者を作ろうとしている。
数学の問題は、式の変形と問題の分解と解の探索の問題に還元されるから、
人工知能でもいくつかの問題を解くことができるはずだ。
- 45 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/28(水) 18:58:35.37 ID:xr03hxaD]
- >>42
はじめは基礎と慣れが大事。不満なら君も出題してもかまわない。
次は集合論から出題したまえ。
- 46 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 19:12:43.24 ID:MQBQj2T8]
- >>44
なぜ集合論？
一応念のためいっとくが>>42は某スレの1(俺)とは別人だぞ。
- 47 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/28(水) 19:42:58.51 ID:xr03hxaD]
- お題：
「Z⊆XかつZ⊆YならばZ⊆X∩Y」を証明せよ。
- 48 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 20:04:26.42 ID:Q7XfmRRj]
- >>43
Coqあるいは片山さんは、東大ロボプロジェクトはどう評価してるの？
- 49 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 20:07:20.02 ID:Q7XfmRRj]
- >>44
集合問題でなく整数問題の系統だが、まずはこういう易しめのお題はどう？
お題：正整数m、nがあり、LCM(m,n) + GCD(m,n) = m + n とする。
このとき、m, n のどちらか一方は、他方によって割り切れることを示せ。
- 50 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 22:31:29.58 ID:MQBQj2T8]
- 易しいっていうけど>>48は>>48の証明をCoqでできるの？
- 51 名前：１３２人目の素数さん mailto:sage [2015/01/29(木) 09:57:12.57 ID:rxXHbRm8]
- 俺はCoqのド素人だから聞いてる。
だが人間にとって証明問題といえばふつうこれくらいからだろ？
- 52 名前：１３２人目の素数さん [2015/01/30(金) 10:46:00.89 ID:NnXyGTxc]
- ☆☆☆☆☆
☆ 自民党、グッジョブですわ。 ☆
www.soumu.go.jp/senkyo/kokumin_touhyou/index.html
☆ 日本国民の皆様方、2016年7月の『第24回 参議院選挙』で、改憲の参議院議員が
3分の2以上を超えると日本国憲法の改正です。皆様方、必ず投票に自ら足を運んでください。
そして、私たちの日本国憲法を絶対に改正しましょう。☆
- 53 名前：１３２人目の素数さん mailto:sage [2015/01/30(金) 11:16:04.23 ID:UCtzINaz]
- >>23
|
 |
