15/01/18 22:30:12.77 Pnbu8M/I.net
人工知能といえばdeep learningとかいうのが流行らしいんだが。
835:１
15/01/20 23:02:01.33 RE29itzd.net
2n=n+nはomegaで一発っぽい。
omegaなしだとどうやるかわからん。
836:デフォルトの名無しさん
15/01/21 01:37:31.40 +/NZ76QF.net
1に餌を与えないでください。
>>425>>559>>655-665
837:片山博文MZ ◆T6xkBnTXz7B0
15/01/21 08:55:01.51 y20qOxOP.net
n＝1×nを使う
838:1
15/01/21 19:32:48.10 83hEDbKu.net
途中よけいなことしてるかもだができたっぽい。
Require Import Arith.
Theorem t:forall n:nat,2*n=n+n.
intros.
replace (2*n) with (n*(S 1)).
symmetry.
replace (n+n) with (n*1+n).
apply mult_n_Sm.
replace (n*1) with (1*n).
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
apply mult_comm.
apply mult_comm.
Qed.
839:１
15/01/21 19:37:49.38 83hEDbKu.net
Coqは一日一時間までにする。
それ以上は自重。
840:１
15/01/21 20:33:19.47 83hEDbKu.net
片山さんの模範解答うｐ希望
841:片山博文MZ ◆T6xkBnTXz7B0
15/01/21 22:08:31.55 OPHJ2hAi.net
>>840
Require Import Arith.
Theorem t: forall n:nat, 2*n = n+n.
intros.
replace (n+n) with (1*n + 1*n).
replace 2 with (1+1).
apply mult_plus_distr_r.
auto.
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
Qed.
842:１
15/01/21 22:49:05.70 83hEDbKu.net
ふーむ。確かに片山さんのほうが自然な証明ですな。
843:片山博文MZ ◆T6xkBnTXz7B0
15/01/23 02:17:55.54 22/uje4h.net
布教のために数学板でも展開するぞ。
【Coq】コンピューターで証明しよう【コック】･2ch.net
ｽﾚﾘﾝｸ(math板)
844:デフォルトの名無しさん
15/10/21 21:08:46.20 qGjQS7QU.net
URLﾘﾝｸ(connect4.game-solver.org)
845:デフォルトの名無しさん
15/10/21 21:49:58.99 kanshW5q.net
ほう、4並べのソルバですか。面白い
なぜこのスレなのかは気にしないでおこう
thx
846:デフォルトの名無しさん
16/05/01 11:01:21.14 tKi6j9CT.net
匿名通信（Tor、i2p等）ができるファイル共有ソフトBitComet（ビットコメット）みたいな、
BitTorrentがオープンソースで開発されています
言語は何でも大丈夫だそうなので、P2P書きたい！って人居ませんか？
Covenantの作者（Lyrise）がそういう人と話したいそうなので、よろしければツイートお願いします
URLﾘﾝｸ(twitter.com)
ちなみにオイラはCovenantの完成が待ち遠しいプログラミングできないアスペルガーｗ
The Covenant Project
概要
Covenantは、純粋P2Pのファイル共有ソフトです
目的
インターネットにおける権力による抑圧を排除することが最終的な目標です。 そのためにCovenantでは、中央に依存しない、高効率で検索能力の高いファイル共有の機能をユーザーに提供します
特徴
Covenant = Bittorrent + Abstract Network + DHT + (Search = WoT + PoW)
接続は抽象化されているので、I2P, Tor, TCP, Proxy, その他を利用可能です
DHTにはKademlia + コネクションプールを使用します
UPnPによってポートを解放することができますが、Port0でも利用可能です(接続数は少なくなります)
検索リクエスト、アップロード、ダウンロードなどのすべての通信はDHT的に分散され、特定のサーバーに依存しません
ｃ