[過去ﾛｸﾞ] 「数学」をプログラミングするには (1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
1(16): 2024/03/16(土)19:41 ID:nuwGv9us(1) AAS
たとえば、プログラミングで
π/4 = 1 - 1/3 + 1/5 - 1/7 + ...
を近似ではなく厳密に確かめるにはどうしたらいいの
人間が証明できるってことは、有限なアルゴリズムに書き換えられると思うんだけど
2(2): 2024/03/16(土)20:29 ID:TBzj9DHS(1) AAS
>>1
証明を記述するための言語がある。CoqとかAgdaとか
あと単発質問はスレを立てるまでもない質問スレでどうぞ
3(2): 2024/03/17(日)07:03 ID:SKDLv/jq(1) AAS
>>1
アルゴリズムではなくメモリ容量の問題
無限小数を求めるには無限のメモリが必要で世界中のメモリを集めても無限にはならないので不可能なだけ
4(1): 2024/03/17(日)11:29 ID:lA2zK95Y(1) AAS
>>3
数学できなさそう
5(1): 2024/03/17(日)12:41 ID:JxXcG9lm(1) AAS
>>3
この問題解くのに無限小数計算してる奴なんかおらんわ（笑）
6: 2024/03/17(日)16:58 ID:t9G995RY(1/2) AAS
数学をプログラミングする方法は、使用するプログラミング言語によって異なりますが、一般的なアプローチは次の通りです。
適切なプログラミング言語の選択: 数学をプログラミングするためには、数値計算やデータ解析に適した言語を選択することが重要です。Python、Julia、MATLAB、Rなどが一般的に使用されます。
必要なライブラリのインポート: 数学的な計算を効率的に行うためには、各言語には数学関連のライブラリが用意されています。例えば、Pythonの場合、NumPyやSciPyが、Juliaの場合、Baseや特定のパッケージが数学関数を提供します。
数学的なアルゴリズムの実装: 数学的なアルゴリズムをプログラミングする際には、基本的な数学的概念やアルゴリズムの理解が必要です。数式をプログラムに変換することが重要です。
データの操作と可視化: 数学をプログラミングする場合、しばしばデータの操作や可視化が必要になります。そのためには、適切なデータ構造や可視化ツールを使用します。
7: 2024/03/17(日)17:46 ID:zKMEHLV8(1/2) AAS
定理証明支援系はオワコン
8: 2024/03/17(日)18:05 ID:QfhdY2k7(1) AAS
ランベルト関数(近似精度がヤヴァくてもヨシ)
をサポートしてる言語のがほしいデス
9: 2024/03/17(日)18:39 ID:zKMEHLV8(2/2) AAS
基礎論以外の命題の証明を証明支援系で一から書くのは現実的ではないから、既存の有名命題がライブラリとして使えるような処理系を使うことになるんだろう
10: 2024/03/17(日)19:26 ID:OVnjvt7h(1) AAS
証明支援系で証明を書いても、それを再利用してべつの定理を自動で証明できるわけでもないし、ソフトウェアとして全く無意味だよね……
11: 2024/03/17(日)19:48 ID:HYzzoyFI(1) AAS
証明支援系を使うことで未知の証明ができたり、数学の問題がよくわかったりするわけじゃなくて、
すでに証明できてるものを、PかつQを表す型はこうで～ みたいな書き換えをやるだけだからな
12(1): 2024/03/17(日)21:15 ID:t9G995RY(2/2) AAS
Condensed Mathematics
外部ﾘﾝｸ:www.math.ku.dk
topologyに対するP. Scholzeの試しみ
13: 2024/03/17(日)22:11 ID:BrUemZnE(1) AAS
証明支援系が役に立たないなら、そもそも数学で証明を与えることにどういう意味があるのか考えてしまう
14: 2024/03/17(日)22:43 ID:zgd3XX/C(1) AAS
厳密だが根拠がない等式を、厳密ではないが根拠のある不等式の集まりにすりかえる
15: 2024/03/18(月)08:21 ID:PIvrnI/y(1) AAS
数==数では背理法が使いにくいが
集合==集合は背理法や不等号の価値がまるで渡米したIT創業者みたいになる
16: 2024/03/18(月)08:43 ID:pTevW9jL(1/3) AAS
イミフ
17: 2024/03/18(月)09:53 ID:dVjvry4m(1/2) AAS
読まなくても分かることをほぼ知り尽くしてから読めば楽に読める
例えば書いた者に悪意があるのかないのかを事前に知らないより知っている方が楽
正義とか悪とかが苦手な人にはこれができない
18: 2024/03/18(月)10:14 ID:HmpJvDlJ(1/2) AAS
∫_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の特殊値がライブラリによって既知なら、書き下せそう
ただ、書いたところでだからなんだって話だが
19: 2024/03/18(月)10:16 ID:pTevW9jL(2/3) AAS
おっさんのポエム
20: 2024/03/18(月)10:19 ID:HmpJvDlJ(2/2) AAS
あとArctanのテイラー展開
もしくは項別積分
項別積分する場合は、べき級数の収束半径とか、境界での連続性とかも
21: 2024/03/18(月)11:21 ID:dVjvry4m(2/2) AAS
積分変数を別名に変えても積分の結果が変わらないこと
などを証明することに興味無さすぎて
変数を使わない技術だけが発達しているんじゃないか
22(1): 2024/03/18(月)17:26 ID:pTevW9jL(3/3) AAS
道師様のお言葉
外部ﾘﾝｸ[pdf]:terrytao.files.wordpress.com
23(1): 2024/03/18(月)20:14 ID:nsefbItQ(1) AAS
>>4
そしてあんたはプログラムができない
永久にすれ違いだなｗ
>>5
実際に計算しない限りプログラムの世界では完成したとは言えない
できたような気になってるだけだｗ
24: 2024/03/18(月)20:38 ID:8wq33qzx(1) AAS
>>23
ふつうに証明支援系で証明できるが
25: 2024/03/18(月)20:59 ID:zv8Td5xB(1/2) AAS
変数に別の変数 (を含む式) を代入するのは嫌なので、右辺を実際に計算してしまった値を代入する
計算してない式を代入するのが何故そんなに嫌なのかを理解しない限り話が進まない
26: 2024/03/18(月)21:35 ID:fpvRWfHG(1) AAS
コード書けない奴が必死に妄想でレスバするクソスレ
ＮＧ決定
27: 2024/03/18(月)23:20 ID:zv8Td5xB(2/2) AAS
しかし、何も書かないより悪いコードを書く方がマシみたいな保証が
あると思うならそれこそ妄想なのでは
28: 2024/03/19(火)04:11 ID:YAmi9Hnz(1) AAS
数学を記述するには一階述語論理があれば十分
しかし処理系側は特殊なケースに特化するよりも自然に実装できる範囲で一般化したほうがいいだろう
命題の記述は依存型による
29(1): 2024/03/19(火)12:34 ID:pUZ6M7m/(1) AAS
動的型付けの証明支援系ってのは何をしてるんだ？
30: 2024/03/19(火)14:33 ID:NSxYSp14(1) AAS
○○を支援する言語と○○が可能な言語を分断するパラダイムはたしかにオワコンだ
逆に支援を語りえない所謂unsafeを書けるやつが比較的新しい
31(1): 2024/03/19(火)15:02 ID:YRVQB5Qs(1) AAS
>2 の紹介しているCoqとか、純粋関数型言語HaskellもPCで動く数学って感じではあるけども、そもそもメモリが有限なので連続を表現できない。
どんなに小さい数を表現できても有限である以上は離散的なのよねん。
離散数学の範囲ならHaskell良いよ。
子供向けだけど、Viscuit(ﾋﾞｽｹｯﾄ)は写像というか変換のみで言語作ってる。
（ビスケットの中の人曰く「書き換え型言語」）
32: 2024/03/19(火)15:24 ID:3KaIc7lk(1) AAS
>>31
ポエムは日記に書いてろ
33(2): 2024/03/19(火)16:20 ID:Q+qUW8xc(1) AAS
leanとかいうソフトで学部レベルの定理の証明をすべて書くとかいうプロジェクトがあるそうですが、そういう証明を見ると勉強する側として勉強になりますか？
34: 2024/03/19(火)16:58 ID:WY0TXEXb(1/3) AAS
>>33
勉強にはなるんじゃない？
35: 2024/03/19(火)16:59 ID:WY0TXEXb(2/3) AAS
ほんとうに教科書に載ってる定理の証明がぜんぶ正しく書かれてるなら、それは教科書読んでるのと同じわけだし
36(2): 2024/03/19(火)17:00 ID:WY0TXEXb(3/3) AAS
lean4はプログラミング言語としても、haskellやrustくらいパワフルな言語なので、cだのfortranだの勉強するよりプログラミングの勉強にもなる
37: 2024/03/19(火)17:06 ID:50xBt2sS(1) AAS
>>29
推論規則にしたがって項を削除したり、条件をみたす要素を深さ優先探索したり
38: 2024/03/19(火)17:54 ID:/7JjNXd8(1) AAS
証明支援系っつっても、ふつうにプログラム書くのと同じで、特定の問題の解法をプログラムしてるだけ
ようは論理のピタゴラスイッチ作ってるだけ
べつに未知の証明を自動で発見してくれるわけではない（もちろん、問題によっては自動的に解決できる場合もあるが）
39: 2024/03/19(火)17:56 ID:P1OcOpxu(1) AAS
証明支援系Lean4
数式処理システムSage
組版システムLaTeX
を組み合わせたオープンソースの統合数学環境と、黒板の文字や図を認識する入力インタフェースがあればいいと思う
40: 2024/03/19(火)18:04 ID:qttME5ET(1) AAS
>>36
「プログラミングの勉強」を「プログラム言語」の勉強だと思ってるバカ
「program」の意味を調べてみろ。言語はただの手法の一つ
41: 2024/03/19(火)18:56 ID:5dhARo0o(1) AAS
バカが必死で草
42: 2024/03/19(火)19:15 ID:IwEkPQSo(1) AAS
この馬鹿は何がしたいんだろ……
43(1): 2024/03/20(水)10:18 ID:ea1o2Ub5(1/4) AAS
>>36
CやFortranの評価が低いということはHaskellの中でモナドの評価が低いよね
それはもったいないから言語を競争させる原理はよくない
44: 2024/03/20(水)12:54 ID:VbUXRLzi(1) AAS
>>43
ポエムはよそで書いてろ
45: 2024/03/20(水)13:10 ID:ea1o2Ub5(2/4) AAS
ミサイルでも撃たれたならともかく
ポエムなるものを書き込まれたことへの反応が過剰なのが気になる
現実世界にポエムが存在しなくなれば消去法で「数学」になるってことなのかな
46: 2024/03/20(水)14:27 ID:I+zqr01r(1) AAS
スレタイが悪い
専門用語や英語を入れておかないと、自分も話題に参加できると勘違いした馬鹿が書き込む
47(1): 2024/03/20(水)15:26 ID:4PdbE3xv(1/3) AAS
仲よき事は美しき哉 志賀直哉
48: 2024/03/20(水)15:27 ID:4PdbE3xv(2/3) AAS
>>22
これに反応できないお前ら
49: 2024/03/20(水)15:50 ID:vNXgKg89(1) AAS
>>47 武者小路実篤じゃなかったっけ
上下前次1-新書関写板覧索設栞歴
あと 953 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 1.436s*