Inter-universal geometryとABC予想(シン応援スレ) 92 (261ﾚｽ)
上下前次1-新
243: 07/17(金)20:06 ID:zMIRi+X7(2/9) AAS
つづき
なお、6で我々は(A)(B)(C)のいずれかが供給されればLEANの形式化と接続して機械検証すると言ってるが、俺は中身はほとんど理解してないので、これは我々と言うよりは純粋にFable5の言い分となる
もし7月17日にLANAプロジェクトでGithubが公開されなければ公開するかもしれんが、Fable5が利用クレジットでの利用じゃなく、再度月額プランのみで使えるようになったらでないとFable5でやるつもりはない他のモデルではやるかもしれん
ちなみに3.11までは特に問題なくLEAN化は成功して、3.11を認めた上でのCor3.12の証明も機械検証は難なく通った
問題はそれがトートロジー的閉ループを構築していることに帰着すること
しかしそれは望月が論文内で言及していて問題ないとする部分でもある
4要請の前の0〜3は以下
0. 一行要旨
IUT 4論文の主張のうち、機械検証(Lean 4)で正しさを確認できた部分と確認できなかった部分の境界が、 [IUTchIV] Thm 1.10 証明 Step (v) の一入力 —— λ := ord(q^{j²}) を受信側正規化の体積計算に適用してよいこと —— に正確に一致した。この入力の導出(定義的措定ではなく)の所在をご教示いただきたい。
1. 背景: 何を検証済みで、何を疑っていないか
省7
上下前次1-新書関写板覧索設栞歴
あと 18 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.012s