26/08/06 10:59:01.23 S7IQGdSL.net
自明だ！の次は自然だ！と言い出しかねない
767:１３２人目の素数さん
26/08/06 21:25:10.03 zf56DTzr.net
>自明
>>14
Peter Scholze, who everyone thinks is the greatest mathematician of this generation, says he cannot deduce 3.12 (which is the ABC conjecture,
in paper #4) from 3.11 (a summary of the first 3 ABC papers) in Mochizuki’s papers.
Koshikawa had a similar problem, and when he asked Mochizuki about it,
the latter responded that the deduction is self.evident.
self.evidentは数学で自明だが、この場合は望月独自のIUT語の可能性が大だろう
(>>231)
768:１３２人目の素数さん
26/08/08 07:51:08.09 fUYTf/8g.net
>>765
・Learn Lean
Lean is a functional programming language and theorem prover built for formalizing math and for formal verification,
but is flexible enough for general coding.
・Leanを学ぶ
Leanは、数学の形式化や形式検証のために開発された関数型プログラミング言語および定理証明器ですが、
一般的なコーディングにも十分活用できる柔軟性を備えています。deepl
769:１３２人目の素数さん
26/08/08 09:47:45.89 BsXbMFt/.net
カリーハワード対応と言って
プログラムの型検査が定理の証明に対応するのよ
比喩とかじゃなくて数学的に同じなんだよ
770:１３２人目の素数さん
26/08/08 10:51:45.01 CXsF+oL7.net
誰か比喩って言った？
型理論において、「型」は「命題」、「型Aから型Bへの写像を記述するブログラム」は「『命題A⇒命題B』の証明」に対応。
771:１３２人目の素数さん
26/08/08 10:59:39.56 BsXbMFt/.net
>>770
被害妄想激しいな
説明しただけだよ
772:１３２人目の素数さん
26/08/08 11:02:11.60 CXsF+oL7.net
論理学と型理論との間だけでなく圏論とも対応関係がある
カリー＝ハワード＝ランベック対応
773:１３２人目の素数さん
26/08/08 11:03:08.47 CXsF+oL7.net
誰も比喩って言ってないのに比喩じゃないと言うのって不自然じゃね？
774:１３２人目の素数さん
26/08/08 11:07:06.55 650UV6Yr.net
暗喩
775:１３２人目の素数さん
26/08/08 11:07:38.14 650UV6Yr.net
が上手
776:１３２人目の素数さん
26/08/08 11:47:59.57 R0q9BDrJ.net
論理式のP→Qとは素朴には
「Pから（必ず）Qが導ける」
ちうことを意味している論理式
プログラミングのP→Qとは素朴には
「P（の元）を入力すると（必ず）Q（の元）が出力される」
ちうプログラム
デカルト閉圏のP→QちうかQ^Pとは
「PからQへの射の全体」
を意味する対象
777:１３２人目の素数さん
26/08/08 11:52:57.08 R0q9BDrJ.net
論理式のP∧Qとは素朴には
「PとQのどちらも成り立つ」
ちうことを意味している論理式
プログラミングのP×Qとは
「P（の元）とQ（の元）の組」
の型
デカルト閉圏のP×Qとは
「P→*←Qのpull back」
を意味する対象
778:１３２人目の素数さん
26/08/08 11:57:05.82 R0q9BDrJ.net
論理式のT（真）とは素朴には
「成立していること」
を意味する論理式
プログラミングのトップ型とは
「プログラミングで考えている凡て」
を想定する型
デカルト閉圏の*とは
すべての対象からの射
「P→*」
がただ1つ存在する対象
779:１３２人目の素数さん
26/08/08 12:33:28.44 R0q9BDrJ.net
これも「モチーフ」チックね
780:１３２人目の素数さん
26/08/08 12:33:50.46 R0q9BDrJ.net
でも具体性あるだけ「モチフ」よりかマシ
781:１３２人目の素数さん
26/08/09 08:09:16.03 onqI+h29.net
>>769
>比喩
川上量生企画望月新一監修加藤文元著IUT本では、(>>
22)
・遠アーベル幾何学は既存の数学
の範囲内。
一方
・IUT理論のように、あまりにも 新奇で斬新なものだったりすると 、通常の言葉に翻訳するには 多くの言葉や概念を 巧みな比喩を 用いて説明するしかありません。
・IUT語 p51
UT理論は、一般的な数学の パラダイムの枠内では語れない、 全く新しいフレームワークと言語・ 概念体系を基盤として構築されている。
782:１３２人目の素数さん
26/08/09 08:15:22.56 onqI+h29.net
また、
Leanは、数学の形式化や形式検証のために開発された関数型プログラミング言語および定理証明器です(>>768)
783:１３２人目の素数さん
26/08/09 11:17:54.60 wj+RJXo8.net
京大病院、脳腫瘍ではなく患者の小脳と脳幹の正常部位を摘出（運動と自発呼吸を司る部位） 患者は生き地獄に [595118796]
URLﾘﾝｸ(greta.5ch.io)
784:１３２人目の素数さん
26/08/09 16:12:28.31 q/CiUH4O.net
ショートスリーパー信者ボコボコにしたら
遠吠えがIUTと同じだったw
785:１３２人目の素数さん
26/08/12 16:50:21.12 pYIMntC/.net
URLﾘﾝｸ(youtu.be)
786:１３２人目の素数さん
26/08/14 17:01:28.54 UTVWYFxL.net
abc予想的なものを説明してるのかと思ったらAIに作らせた間違ってる画像をこれは気にしないでくださいとか言ってる死にそうなリハッククオリティ