Interuniversal geometry とABC 予想61
(239ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) 自ID ﾚｽ栞 あぼーん
89: 07/17(金)12:20 ID:dythpcIC(1/10) AAS
肝心のLEANは？
94: 07/17(金)13:17 ID:dythpcIC(2/10) AAS
PDF中に7月17日に公開されたLEANの解説ってあるけどGithubの URLとか微塵もないな
あとLANAでは体積計算を比較するpilot volume dataを構成する二つの経路が一致してるって証明がないらしいが、ワイのFable5のLEANコードでは結局IUT4のthm1.10でq^j^2の証明がないってとこで止まっとるけど経路の証明枠組みそのものは揃ってるってClaudeは言っとるな
まぁあってるかは知らんがな
95: 07/17(金)13:27 ID:dythpcIC(3/10) AAS
てか一部がAIによってかかれとるって宣言しとるな
全部AIの俺のとほぼ同じやない？
どうせ人間が関わっとる部分極小だろ
Fable5使ってる分俺のLEANの方が上まであるぞこれ
97: 07/17(金)13:47 ID:dythpcIC(4/10) AAS
結局ケドラヤが言っとるように鍵になるのは望月新一の言うとこのトートロジー的閉ループを証明が構成しとることよな
俺のプロジェクトのFable5の言い分と一緒やわ
98(1): 07/17(金)13:51 ID:dythpcIC(5/10) AAS
ん？？？LEAN公開しないのん？？めんどくせー俺の公開したくないんだが…公式で途中だからって出さないとか無能かよ
104(4): 07/17(金)14:18 ID:dythpcIC(6/10) AAS
LANAプロジェクトに一定の敬意を払いつつも
逃げ腰でLEANの公開なしってのは流石にどうかと思ったから俺のOpus4.8とFable5で作った
プロトタイプ、スケルトン、未完成、言い方は何でも良いが公開しとくわ
コメントはほぼ日本語なんで海外勢向けではないがな
まぁAIに読み込ませてコメント英語化するとか容易だろうし許せ
外部ﾘﾝｸ:github.com
105: 07/17(金)14:20 ID:dythpcIC(7/10) AAS
Githubの使い方もあまり分かってないから公開方法も適当だが許せ
106(1): 07/17(金)14:30 ID:dythpcIC(8/10) AAS
こっちにも貼っとく
Opus4.8とFable5で作ったIUTの形式化
外部ﾘﾝｸ:github.com
107: 07/17(金)14:31 ID:dythpcIC(9/10) AAS
あぁスレミスったごめん
169: 07/17(金)23:25 ID:dythpcIC(10/10) AAS
結局、遠アーベル幾何学とLEAN両方を理解できる存在がいないことに尽きるな
世界に20人いないんじゃね？
だからコメリンも会見で散々AIエージェントAIエージェント言ってたように、AIに頼った証明構築になっていくんじゃねーの？
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.535s*