[過去ﾛｸﾞ]
「数学」をプログラミングするには (1002ﾚｽ)
「数学」をプログラミングするには http://mevius.5ch.net/test/read.cgi/tech/1710585705/
上
下
前
次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
15: デフォルトの名無しさん [sage] 2024/03/18(月) 08:21:20.80 ID:PIvrnI/y 数==数では背理法が使いにくいが 集合==集合は背理法や不等号の価値がまるで渡米したIT創業者みたいになる http://mevius.5ch.net/test/read.cgi/tech/1710585705/15
16: デフォルトの名無しさん [sage] 2024/03/18(月) 08:43:53.53 ID:pTevW9jL イミフ http://mevius.5ch.net/test/read.cgi/tech/1710585705/16
17: デフォルトの名無しさん [sage] 2024/03/18(月) 09:53:36.41 ID:dVjvry4m 読まなくても分かることをほぼ知り尽くしてから読めば楽に読める 例えば書いた者に悪意があるのかないのかを事前に知らないより知っている方が楽 正義とか悪とかが苦手な人にはこれができない http://mevius.5ch.net/test/read.cgi/tech/1710585705/17
18: デフォルトの名無しさん [] 2024/03/18(月) 10:14:54.25 ID:HmpJvDlJ ∫_0^1 dx/(1 + x^2) = Arctan(1) - Arctan(0) = π/4 x = arctan(y) x' = 1/y' = cos(x)^2 = cos(x)^2/(cos(x)^2 + sin(x)^2) = 1/(1 + tan(x)^2) = 1/(1 + y^2) 微分とtanの特殊値がライブラリによって既知なら、書き下せそう ただ、書いたところでだからなんだって話だが http://mevius.5ch.net/test/read.cgi/tech/1710585705/18
19: デフォルトの名無しさん [sage] 2024/03/18(月) 10:16:03.73 ID:pTevW9jL おっさんのポエム http://mevius.5ch.net/test/read.cgi/tech/1710585705/19
20: デフォルトの名無しさん [] 2024/03/18(月) 10:19:41.06 ID:HmpJvDlJ あとArctanのテイラー展開 もしくは項別積分 項別積分する場合は、べき級数の収束半径とか、境界での連続性とかも http://mevius.5ch.net/test/read.cgi/tech/1710585705/20
21: デフォルトの名無しさん [sage] 2024/03/18(月) 11:21:23.44 ID:dVjvry4m 積分変数を別名に変えても積分の結果が変わらないこと などを証明することに興味無さすぎて 変数を使わない技術だけが発達しているんじゃないか http://mevius.5ch.net/test/read.cgi/tech/1710585705/21
22: デフォルトの名無しさん [sage] 2024/03/18(月) 17:26:37.63 ID:pTevW9jL 道師様のお言葉 https://terrytao.files.wordpress.com/2024/03/machine-jan-3.pdf http://mevius.5ch.net/test/read.cgi/tech/1710585705/22
23: デフォルトの名無しさん [sage] 2024/03/18(月) 20:14:54.78 ID:nsefbItQ >>4 そしてあんたはプログラムができない 永久にすれ違いだなｗ >>5 実際に計算しない限りプログラムの世界では完成したとは言えない できたような気になってるだけだｗ http://mevius.5ch.net/test/read.cgi/tech/1710585705/23
24: デフォルトの名無しさん [] 2024/03/18(月) 20:38:29.54 ID:8wq33qzx >>23 ふつうに証明支援系で証明できるが http://mevius.5ch.net/test/read.cgi/tech/1710585705/24
25: デフォルトの名無しさん [sage] 2024/03/18(月) 20:59:25.05 ID:zv8Td5xB 変数に別の変数 (を含む式) を代入するのは嫌なので、右辺を実際に計算してしまった値を代入する 計算してない式を代入するのが何故そんなに嫌なのかを理解しない限り話が進まない http://mevius.5ch.net/test/read.cgi/tech/1710585705/25
26: デフォルトの名無しさん [] 2024/03/18(月) 21:35:55.83 ID:fpvRWfHG コード書けない奴が必死に妄想でレスバするクソスレ ＮＧ決定 http://mevius.5ch.net/test/read.cgi/tech/1710585705/26
27: デフォルトの名無しさん [sage] 2024/03/18(月) 23:20:36.59 ID:zv8Td5xB しかし、何も書かないより悪いコードを書く方がマシみたいな保証が あると思うならそれこそ妄想なのでは http://mevius.5ch.net/test/read.cgi/tech/1710585705/27
28: デフォルトの名無しさん [] 2024/03/19(火) 04:11:20.65 ID:YAmi9Hnz 数学を記述するには一階述語論理があれば十分 しかし処理系側は特殊なケースに特化するよりも自然に実装できる範囲で一般化したほうがいいだろう 命題の記述は依存型による http://mevius.5ch.net/test/read.cgi/tech/1710585705/28
29: デフォルトの名無しさん [] 2024/03/19(火) 12:34:54.32 ID:pUZ6M7m/ 動的型付けの証明支援系ってのは何をしてるんだ？ http://mevius.5ch.net/test/read.cgi/tech/1710585705/29
30: デフォルトの名無しさん [sage] 2024/03/19(火) 14:33:42.20 ID:NSxYSp14 ○○を支援する言語と○○が可能な言語を分断するパラダイムはたしかにオワコンだ 逆に支援を語りえない所謂unsafeを書けるやつが比較的新しい http://mevius.5ch.net/test/read.cgi/tech/1710585705/30
31: デフォルトの名無しさん [] 2024/03/19(火) 15:02:06.03 ID:YRVQB5Qs >2 の紹介しているCoqとか、純粋関数型言語HaskellもPCで動く数学って感じではあるけども、そもそもメモリが有限なので連続を表現できない。 どんなに小さい数を表現できても有限である以上は離散的なのよねん。 離散数学の範囲ならHaskell良いよ。 子供向けだけど、Viscuit(ﾋﾞｽｹｯﾄ)は写像というか変換のみで言語作ってる。 （ビスケットの中の人曰く「書き換え型言語」） http://mevius.5ch.net/test/read.cgi/tech/1710585705/31
32: デフォルトの名無しさん [] 2024/03/19(火) 15:24:32.49 ID:3KaIc7lk >>31 ポエムは日記に書いてろ http://mevius.5ch.net/test/read.cgi/tech/1710585705/32
33: デフォルトの名無しさん [] 2024/03/19(火) 16:20:03.06 ID:Q+qUW8xc leanとかいうソフトで学部レベルの定理の証明をすべて書くとかいうプロジェクトがあるそうですが、そういう証明を見ると勉強する側として勉強になりますか？ http://mevius.5ch.net/test/read.cgi/tech/1710585705/33
34: デフォルトの名無しさん [] 2024/03/19(火) 16:58:20.60 ID:WY0TXEXb >>33 勉強にはなるんじゃない？ http://mevius.5ch.net/test/read.cgi/tech/1710585705/34
35: デフォルトの名無しさん [] 2024/03/19(火) 16:59:03.63 ID:WY0TXEXb ほんとうに教科書に載ってる定理の証明がぜんぶ正しく書かれてるなら、それは教科書読んでるのと同じわけだし http://mevius.5ch.net/test/read.cgi/tech/1710585705/35
36: デフォルトの名無しさん [] 2024/03/19(火) 17:00:04.15 ID:WY0TXEXb lean4はプログラミング言語としても、haskellやrustくらいパワフルな言語なので、cだのfortranだの勉強するよりプログラミングの勉強にもなる http://mevius.5ch.net/test/read.cgi/tech/1710585705/36
37: デフォルトの名無しさん [] 2024/03/19(火) 17:06:08.09 ID:50xBt2sS >>29 推論規則にしたがって項を削除したり、条件をみたす要素を深さ優先探索したり http://mevius.5ch.net/test/read.cgi/tech/1710585705/37
38: デフォルトの名無しさん [] 2024/03/19(火) 17:54:01.83 ID:/7JjNXd8 証明支援系っつっても、ふつうにプログラム書くのと同じで、特定の問題の解法をプログラムしてるだけ ようは論理のピタゴラスイッチ作ってるだけ べつに未知の証明を自動で発見してくれるわけではない（もちろん、問題によっては自動的に解決できる場合もあるが） http://mevius.5ch.net/test/read.cgi/tech/1710585705/38
39: デフォルトの名無しさん [] 2024/03/19(火) 17:56:38.86 ID:P1OcOpxu 証明支援系Lean4 数式処理システムSage 組版システムLaTeX を組み合わせたオープンソースの統合数学環境と、黒板の文字や図を認識する入力インタフェースがあればいいと思う http://mevius.5ch.net/test/read.cgi/tech/1710585705/39
ﾒﾓ帳
(0/65535文字)
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
あと 963 ﾚｽあります
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.019s