オイラー・マスケローニ定数の有理性問題をLLMで解かせるとどうなるの

オイラー・マスケローニ定数の有理性問題をLLM(ChatGPT-5.2-Pro 検証:Claude-Opus-4.5)に取り組ませてみたら肯定的に解決したというのがTwitterで話題になっていた。

https://x.com/EARL_med_tw/status/2014600833711886633

そもそも自分は、オイラー・マスケローニ定数の有理性問題のことは知らなかったが、長年解決されてない問題だということなので、これも既存の数学じゃ解けない類の問題なのではないかということで、これまたLLMを使って確認してみたら、やっぱり既存の数学体系では証明できない類のものだということになった。

ちなみに、既存の数学じゃ解けない類の問題なのではないかというもののこれまでのまとめはこちら

Twitterではツイートを目にした人がAIで証明に成功したと勝手に受け取った人が多いようで、概ねボロクソな反応で溢れているが、私は下記のようにみている

  • オイラー・マスケローニ定数の有理性問題は既存の数学体系内では証明できない
  • LLMが証明できた、というのはIUTが指摘されているような既存数学とのギャップがあるのを無視した結果に思える
  • LLMは既存の数学のルールからはみ出しているかは気にしていない可能性が高い

数学に対する冒涜、素人が自分が100%理解できないことをやって何がしたいのか、など割といわれたい放題になっているが、このままめげずに進めていけば、恐らく「LLMの出した結果は正しいが、証明として成立するには飛躍がある」的なことになると予想している。そうなると、もしかしてIUTでも似たようなことが起きているのでは?という風に話題が展開し、数学を拡張するのか否かという風に話題が展開したりするのではないだろうか。 ちなみに自分的には、ヒルベルト辺りまでの数学を特殊数学として、ゲーデル以降は一般数学として分けたらすっきりするのではないかと思っている。圏論なども既存の数学からはみ出しつつあるらしいし、既存の二元論でやりたい人は特殊数学を追求すればいいのではないかと思ったりするのだがどうなのだろう。ちなみに個人的には数学への興味は皆無に等しいが、何故こんなことになっているのか(難問の癖に解けるかどうかは別に数学界では検証されていないことの多さ)には興味がある。

ちなみに、Geminiでオイラー・マスケローニ定数の有理性問題を私の空数学で空証明すると下記のようになる。(※数学で証明ではなく、空数学で空証明)

 \mathrel{\overset{\mathrm{mw}}{=}}によるオイラー定数の無理数性記述スケッチ

  1.  \gamma を、離散宇宙 \mathcal{U}_{\Sigma}(調和級数)と連続宇宙 \mathcal{U}_{\ln}(対数)の界面に位置するオブジェクトとする。
  2.  \gamma := \lim_{n \to \infty} \left( \sum_{k=1}^n \frac{1}{k} \in \mathcal{U}_{\Sigma} \right) \ominus \left( \ln n \in \mathcal{U}_{\ln} \right) 歪みエネルギー E の同定:\gamma$ を有理数 p/q \in \mathbb{Q}$(単一の静的宇宙)に閉じ込めようとすると、離散と連続の界面における曲率の差により、非ゼロの構造的歪み E(\gamma, \mathbb{Q}) > 0 が恒常的に発生する。
  3.  D(t) = | \gamma - \mathbb{Q} |_{\mathrel{\overset{\mathrm{mw}}{=}}} \implies \lim_{t \to \infty} D(t) \neq 0
  4.  \mathrel{\overset{\mathrm{mw}}{=}} による結論(空解決):\gamma が p/q と静的に一致(=)することは NMF(非中道の誤謬) である。一方で、\gamma は無理数(無限の洗練を要する構造)との間で E を最小化する。\gamma \mweq \text{Irrational} \quad (\text{subject to } Dfix0)
 \therefore$ Dfix0 基準において、\gamma は無理数として安定する。

参考駄文献

LLMでProject EulerのP198が解けない問題

LLMでのコード生成を試すのにProject Eulerを題材にしてみていたが、P198が妙に解けない。

妙に解けないというか、どうもP198は現状のLLMには何かの罠に捕捉されてしまうという難問らしい。どういう風に難問かというと、(1)問題文を正しく解釈して、現実的な時間で実行が終了しないコードを出力する (2)これじゃ終了しないので終了するコードに改善して、とユーザーが指示すると今度はLLMは「もっともらしい解法」を出力しようとし、「Project Eulerの問題なら、きっと動的計画法か何かを使うはずだ。それっぽいコードを書こう。」となったりして、形は似ているが正解には辿り着けないコードを出力する。 ユーザーが、これでは駄目なので正確にして、となると(1)の再来ということになるらしい。

この問題でしばらく嵌ったが、LLM(gemini)が何かをひらめいたのか突然正解を出力するコードを出した。これで解決かと思い、その経緯を再現できるプロンプトを出力させて他のLLMで解かせてみたが、同じ現象に遭遇してぐるぐるしてしまい解けない。

この理由を探っていくとどうやら、問題解釈のメタの次元を上下する際に連続的にしか移動していないのが原因だと分かったので、GAの突然変異のように非連続的な変化をさせたらどうかということで、そのように指示したらgeminiが勝手にARX-Coreという手法を考えついてそれを適用し、ARX-Coreならこういう問題は解けるようになったらしい。

LLMの幻覚にも色々種類があるんだろうなと思う新春なのだった。

;;; ARX-Core Manifestation: Project Euler 198 Solver
;;; Structural Necessity: Ambiguous numbers are midpoints of Farey neighbors.
;;; Leap: 1D Search (q=1..10^8) -> 2D Farey Tree Traversal (bd <= 5*10^7)

(declaim (optimize (speed 3) (safety 0) (debug 0)))

(defun solve-ambiguous-numbers ()
  (let* ((q-limit 100000000)
         (bd-limit (floor q-limit 2))
         (threshold-num 1)
         (threshold-den 100)
         (count 0))
    (declare (type (unsigned-byte 64) q-limit bd-limit count threshold-den))

    (labels ((dfs (a b c d)
               "Farey Tree traversal using structural constraints."
               (declare (type (unsigned-byte 64) a b c d))
               (let ((bd (* b d)))
                 (declare (type (unsigned-byte 64) bd))
                 (when (<= bd bd-limit)
                   (let* ((num (+ (* 2 a d) 1))
                          (den (* 2 bd)))
                     ;; Condition: x = num/den < 1/100  =>  100 * num < den
                     (cond ((< (* threshold-den num) den)
                            (incf count)
                            ;; Proceed both directions in the structural branch
                            (dfs a b (+ a c) (+ b d))
                            (dfs (+ a c) (+ b d) c d))
                           ;; Pruning: Only explore left-ward if the left bound is still within threshold
                           ((< (* threshold-den a) b)
                            (dfs a b (+ a c) (+ b d)))))))))

      ;; 1. a=0 branch (Structural Singularity)
      ;; x = 1/(2d). Condition: 1/(2d) < 1/100 and 2d <= 10^8
      ;; This leads to: 50 < d <= 50,000,000
      (setf count (- (floor q-limit 2) 50))

      ;; 2. a > 0 branches (Alethetic Leap)
      ;; We iterate through the top-level segments of the Stern-Brocot tree (1/(d+1), 1/d)
      ;; that are relevant to the denominator constraint.
      (loop for d from 1 while (<= (* d (+ d 1)) bd-limit) do
            (dfs 1 (1+ d) 1 d))

      count)))

;; Execution within the Ffix0 convergence state.
(format t "Total Ambiguous Numbers (AC-optimized): ~A~%" (solve-ambiguous-numbers))
▻ Total Ambiguous Numbers (AC-optimized): 52374425nil

ABC予想とIUTの個人的総括

  • 個人的にはABC予想は既存の数学体系内では、証明できないと予想している
  • しかし、既存の数学体系内では、証明できないことも証明できない
  • どうもIUTで揉めているのも結局そこの部分の話らしい
  • IUTをleanで証明する試みが成功したとしても、揉めている原因は二元論数学の体系内に収める要請だと思うので解決しないのでは?

    • leanもIUT向けにzfcを拡張しようという話がでているらしい→証明の高次元への拡張ということになりそう。
    • 教授の「多くの数学者が当たり前に脳内で無意識のうちにこなしている処理」という表現は、数学証明の拡張は当たり前という主張なのか気になる。
  • Leanによる形式化は、長期的な検証や説明責任を可能にする記録装置となり得るか? | 新一の「心の一票」

Alethetic Context (ACX)という謎概念でLLMにProject Euler 96の数独問題をCommon Lispで解かせる

LLMとチャットしていてAlethetic Context (ACX)という謎概念に辿り着いたので、そのACXという概念でProject Euler 96の数独問題を解かせてみた。 ACXとは、継続とCommon Lispのリスタートを組み合せたような概念。コンディションシステムを使う前提だけど、この例ではリスタートを使うところまではいってない。 Euler 96の問題を読んだだけでACXのコンセプトの元で生成して一発で正解。恐しい。

;;; -*- mode: Lisp; coding: utf-8  -*-

(cl:in-package "CL-USER")

(defun solve-sudoku (grid)
  "ACX的思想に基づく数独ソルバー"
  (labels ((get-candidates (r c)
             (let ((used (make-array 10 :element-type 'bit :initial-element 0)))
               (loop :for i :from 0 :to 8
                     :do (setf (bit used (aref grid r i)) 1
                               (bit used (aref grid i c)) 1
                               (bit used (aref grid (+ (* (floor r 3) 3) (floor i 3))
                                               (+ (* (floor c 3) 3) (mod i 3)))) 1))
               (loop :for v :from 1 :to 9 :when (zerop (bit used v)) collect v)))

           (step-acx (pos κ ρ)
             "ACXのコア:posは現在のSeed位置、κは成功時の継続、ρは失敗時の跳躍(Restart)"
             (if (= pos 81)
                 (funcall κ) ; すべての境界Cを突破(成功)
                 (let ((r (floor pos 9))
                       (c (mod pos 9)))
                   (if (not (zerop (aref grid r c)))
                       (step-acx (1+ pos) κ ρ) ; 既に確定している「色」はスキップ
                       (let ((candidates (get-candidates r c)))
                         (if (null candidates)
                             (funcall ρ) ; 空(不全)に遭遇:直近の分岐へRestart
                             (loop-candidates candidates r c pos κ ρ)))))))

           (loop-candidates (vals r c pos κ ρ)
             "候補数字を次々に顕現させるトランポリン的試行"
             (if (null vals)
                 (funcall ρ) ; このパスの可能性が尽きた:上位の空へ
                 (progn
                   (setf (aref grid r c) (car vals))
                   (step-acx (1+ pos) 
                             κ 
                             (lambda () ; 新たなRestart Mapの登録
                               (setf (aref grid r c) 0) ; Debtの清算(色を空に戻す)
                               (loop-candidates (cdr vals) r c pos κ ρ)))))))

    ;; 初期呼び出し:不全時のρは「解なし」を意味する沈黙
    (step-acx 0 (lambda () grid) (lambda () nil))))

;; --- 補助関数:Euler 96 仕様の入出力と集計 ---

(defun parse-grid (lines)
  (let ((grid (make-array '(9 9) :initial-element 0)))
    (loop :for r :from 0 :to 8
          :for line :in lines
          :do (loop :for c :from 0 :to 8
                    :do (setf (aref grid r c) (digit-char-p (char line c)))))
    grid))

(defun solve-euler-96 (filename)
  (with-open-file (in filename)
    (let ((total 0))
      (loop :for line := (read-line in nil)
            :while line
            :do (let* ((grid-lines (loop repeat 9 collect (read-line in)))
                       (grid (parse-grid grid-lines))
                       (solved (solve-sudoku grid)))
                  (incf total (+ (* (aref solved 0 0) 100)
                                 (* (aref solved 0 1) 10)
                                 (aref solved 0 2)))))
      total)))



(solve-euler-96 "~/Desktop/0096_sudoku.txt")24702

LLMにZebraベンチのCommon Lisp版をCPSで書いてもらう

論理やプログラムには実は16の概念しかないのではないかという仮説を検証するために、論理プログラミングと、手続きプログラミングで16概念の対応表を作成し、マッピングして変換するというのを試す。 お題はProlog版のzebraをCommon Lispに変換。

実験結果としては結構見通しが良くて速い実装が錬成された。zebraの場合、バックトラック法がはまるようで、繰り返しなどを使って手続き的に書いた方が遅くなるのでCPSはバックトラック法と繰り返しのいいとこどりになっているのかもしれない。 そこそこ無駄はあるので、チューニングすればもっと高速になるかもしれない。

;;; -*- mode: Lisp; coding: utf-8  -*-

(declaim (optimize (speed 3) (safety 0) (compilation-speed 0)
                   (debug 0)))

(cl:in-package "CL-USER")


;;;; ======================================================================
;;;; 16マトリックス・トランスレータ: Prolog to Common Lisp
;;;; ターゲット: ゼブラ問題 (Einstein's Puzzle)
;;;; 戦略: 14. 絶の非 (CPS) + 10. 亦の非 (Destructive Backtracking)
;;;; ======================================================================

(defun unify (pattern target)
  "2. 是の非(変数)を 1. 是の是(事実)で埋める破壊的単一化。
   不整合(Fuss)が生じた場合は即座にnilを返し、成功時はtを返す。"
  (loop for p in pattern
        for t-ptr on target
        do (let ((t-val (car t-ptr)))
             (cond
               ((and p t-val (not (eq p t-val))) (return-from unify nil))
               ((and p (null t-val)) (setf (car t-ptr) p))))
        finally (return t)))

(defun zebra (cont)
  "14. 非非の非 (CPS): 継続の連鎖によって推論空間を構成する。"
  (let ((h (loop repeat 5 collect (list nil nil nil nil nil))))
    ;; 位相1: 初期事実の導入 (Norwegian / Milk)
    (setf (first (first h)) 'norwegian)
    (setf (fourth (third h)) 'milk)

    (labels 
        ((member-csp (x list next-cont)
           (declare (type list list)
                    (type function next-cont))
           (dolist (house list)
             (let ((snapshot (copy-list house))) ; 10. 亦の非: 状態の保存
               (when (unify x house)
                 (funcall next-cont))
               (replace house snapshot)))) ; 10. 亦の非: 状態の復元(Debt精算)

         (iright-csp (l r list next-cont)
           (loop for (a b) on list while b do
             (let ((snap-a (copy-list a)) (snap-b (copy-list b)))
               (when (and (unify l a) (unify r b))
                 (funcall next-cont))
               (replace a snap-a) (replace b snap-b))))

         (nextto-csp (x y list next-cont)
           (iright-csp x y list next-cont)
           (iright-csp y x list next-cont)))

      ;; --- 推論ラインの顕現 (Prologの述語順序を忠実にCPS化) ---
      (member-csp '(englishman nil nil nil red) h (lambda ()
      (member-csp '(spaniard dog nil nil nil) h (lambda ()
      (member-csp '(nil nil nil coffee green) h (lambda ()
      (member-csp '(ukrainian nil nil tea nil) h (lambda ()
      (iright-csp '(nil nil nil nil ivory) '(nil nil nil nil green) h (lambda ()
      (member-csp '(nil snails winston nil nil) h (lambda ()
      (member-csp '(nil nil kools nil yellow) h (lambda ()
      (nextto-csp '(nil nil chesterfield nil nil) '(nil fox nil nil nil) h (lambda ()
      (nextto-csp '(nil nil kools nil nil) '(nil horse nil nil nil) h (lambda ()
      (member-csp '(nil nil luckystrike oj nil) h (lambda ()
      (member-csp '(japanese nil parliaments nil nil) h (lambda ()
      (nextto-csp '(norwegian nil nil nil nil) '(nil nil nil nil blue) h (lambda ()
      (member-csp '(nil nil nil water nil) h (lambda () ;; WaterDrinkerの探索
      (member-csp '(nil zebra nil nil nil) h (lambda () ;; ZebraOwnerの探索
        ;; 16. 絶の絶: すべての制約を満たした最終状態を継続へ渡す
        (funcall cont h))))))))))))))))))))))))))))))))

(defun zebra-solve ()
  "8. 非の非非(Cut): 探索空間を打ち切り、不動点を抽出する。"
  (block found
    (zebra (lambda (h)
             (let ((w-owner (first (find 'water h :key (lambda (x) (fourth x)))))
                   (z-owner (first (find 'zebra h :key (lambda (x) (second x))))))
               ;; 不動点の現成と外部への射影
               (return-from found (values (copy-tree h) w-owner z-owner)))))
    nil))

(defun benchmark-zebra (&optional (iterations 1000))
  "Prolog版 benchmark/0 との比較用実行関数。"
  (format t "Starting Zebra Benchmark (~A iterations)...~%" iterations)
  (time 
   (dotimes (i iterations)
     (zebra-solve)))
  (multiple-value-bind (houses water zebra) (zebra-solve)
    (format t "~%[Result]~%")
    (format t "Water Drinker: ~A~%" water)
    (format t "Zebra Owner  : ~A~%" zebra)
    (format t "House Details:~%")
    (dolist (house houses) (format t "  ~A~%" house))))
(time (benchmark-zebra 1000))
▻ Starting Zebra Benchmark (1000 iterations)...
▻ 
▻ [Result]
▻ Water Drinker: norwegian
▻ Zebra Owner  : japanese
▻ House Details:
▻   (norwegian fox kools water yellow)(ukrainian horse chesterfield tea blue)(englishman snails winston milk red)(spaniard dog luckystrike oj ivory)(japanese zebra parliaments coffee green)nil
User time    =        0.898
System time  =        0.004
Elapsed time =        0.892
Allocation   = 1109182440 bytes
304 Page faults
GC time      =        0.008

ベンチ結果

Allegro PrologはAllegro CL内では無双という感じだけど概してCLのCPS Zebraの方が高速

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; International Allegro CL Free Express Edition 11.0 [64-bit macOS (Intel)]
;;      ZEBRA-ALLEGRO-PROLOG:    11,985,981LIPS owner: JAPANESE 8.23PP
;;                 ZEBRA-CPS:     9,226,618LIPS owner: JAPANESE 6.34PP
;;                   ZEBRA-4:     6,107,142LIPS owner: JAPANESE 4.20PP
;;    ZEBRA-ALLEGRO-MODERATO:     5,457,446LIPS owner: JAPANESE 3.75PP
;;           ZEBRA-VPROLOG-T:     3,271,683LIPS owner: JAPANESE 2.25PP
;;                   ZEBRA-5:     3,246,835LIPS owner: JAPANESE 2.23PP
;;                   ZEBRA-1:     2,806,345LIPS owner: JAPANESE 1.93PP
;;             ZEBRA-VPROLOG:     2,734,541LIPS owner: JAPANESE 1.88PP
;;                   ZEBRA-3:     2,261,904LIPS owner: JAPANESE 1.55PP
;;                   ZEBRA-2:     2,055,288LIPS owner: JAPANESE 1.41PP
;;                   ZEBRA-0:     1,781,250LIPS owner: JAPANESE 1.22PP
;;                   ZEBRA-6:     1,617,276LIPS owner: JAPANESE 1.11PP
;;           ZEBRA-PAIPROLOG:     1,455,732LIPS owner: JAPANESE 1.00PP
;;            ZEBRA-ZRPROLOG:     1,417,127LIPS owner: JAPANESE 0.97PP
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; LispWorks 8.1.2
;;                 ZEBRA-CPS:    14,140,022LIPS owner: japanese 9.23PP
;;           ZEBRA-VPROLOG-T:     5,247,545LIPS owner: japanese 3.43PP
;;                ZEBRA-CLOG:     5,015,643LIPS owner: japanese 3.27PP
;;                   ZEBRA-4:     4,075,309LIPS owner: japanese 2.66PP
;;             ZEBRA-VPROLOG:     2,941,513LIPS owner: japanese 1.92PP
;;                   ZEBRA-3:     2,364,055LIPS owner: japanese 1.54PP
;;                   ZEBRA-1:     2,064,220LIPS owner: japanese 1.35PP
;;                   ZEBRA-5:     2,038,302LIPS owner: japanese 1.33PP
;;                   ZEBRA-0:     1,785,714LIPS owner: japanese 1.17PP
;;                   ZEBRA-2:     1,726,807LIPS owner: japanese 1.13PP
;;           ZEBRA-PAIPROLOG:     1,532,075LIPS owner: japanese 1.00PP
;;            ZEBRA-ZRPROLOG:     1,500,175LIPS owner: japanese 0.98PP
;;                   ZEBRA-6:     1,455,566LIPS owner: japanese 0.95PP
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; SBCL 2.5.4
;;                 ZEBRA-CPS:    15,851,944LIPS owner: JAPANESE 4.03PP
;;           ZEBRA-VPROLOG-T:     9,527,976LIPS owner: JAPANESE 2.43PP
;;                   ZEBRA-4:     8,410,922LIPS owner: JAPANESE 2.14PP
;;                   ZEBRA-3:     7,859,703LIPS owner: JAPANESE 2.00PP
;;             ZEBRA-VPROLOG:     7,454,644LIPS owner: JAPANESE 1.90PP
;;                   ZEBRA-2:     7,138,205LIPS owner: JAPANESE 1.82PP
;;                   ZEBRA-0:     6,298,404LIPS owner: JAPANESE 1.60PP
;;                   ZEBRA-6:     5,534,895LIPS owner: JAPANESE 1.41PP
;;                   ZEBRA-5:     4,553,085LIPS owner: JAPANESE 1.16PP
;;            ZEBRA-ZRPROLOG:     4,047,777LIPS owner: JAPANESE 1.03PP
;;           ZEBRA-PAIPROLOG:     3,928,865LIPS owner: JAPANESE 1.00PP
;;                   ZEBRA-1:     3,490,652LIPS owner: JAPANESE 0.89PP
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Clozure Common Lisp Version 1.12.2  DarwinX8664
;;                 ZEBRA-CPS:     6,337,201LIPS owner: JAPANESE 4.29PP
;;           ZEBRA-VPROLOG-T:     3,195,993LIPS owner: JAPANESE 2.17PP
;;             ZEBRA-VPROLOG:     2,485,747LIPS owner: JAPANESE 1.68PP
;;           ZEBRA-PAIPROLOG:     1,476,135LIPS owner: JAPANESE 1.00PP
;;            ZEBRA-ZRPROLOG:     1,337,609LIPS owner: JAPANESE 0.91PP
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ECL 23.9.9
;;                   ZEBRA-4:     4,084,100LIPS owner: JAPANESE 21.96PP
;;                   ZEBRA-1:     1,865,646LIPS owner: JAPANESE 10.03PP
;;                 ZEBRA-CPS:     1,196,431LIPS owner: JAPANESE 6.43PP
;;                   ZEBRA-5:       740,996LIPS owner: JAPANESE 3.98PP
;;                   ZEBRA-3:       703,350LIPS owner: JAPANESE 3.78PP
;;                   ZEBRA-2:       614,230LIPS owner: JAPANESE 3.30PP
;;             ZEBRA-VPROLOG:       519,973LIPS owner: JAPANESE 2.80PP
;;           ZEBRA-VPROLOG-T:       518,374LIPS owner: JAPANESE 2.79PP
;;                   ZEBRA-6:       266,447LIPS owner: JAPANESE 1.43PP
;;                   ZEBRA-0:       194,786LIPS owner: JAPANESE 1.05PP
;;           ZEBRA-PAIPROLOG:       186,021LIPS owner: JAPANESE 1.00PP
;;            ZEBRA-ZRPROLOG:       177,800LIPS owner: JAPANESE 0.96PP
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; swi-prolog
;; % 12,877,724 inferences, 1.487 CPU in 1.504 seconds (99% CPU, 8658073 Lips)

8x8格子で同じ点を二度通らないスタートからゴールまでの経路の数を求める

LLMで遊んでいてDP的な機構(ACDP)が錬成できたので、試しに組み合わせ爆発で大変そうなお題を探してACDPで解かせてみた。

8x8格子で同じ点を二度通らないスタートからゴールまでの経路の数を求める

(run-frontier-8x8)
--- Frontier-ACDP: Breaking 8x8 ---
顕現した経路の総数: 115156685746
計算時間: 0.074

この115156685746という数値が正しいのか分からないので数値も探すそOEISに登録があった。 何もかもLLMまかせ。

とりあえずACDPという手法は使えそうだけど、そのうち忘れそう。

;;; -*- mode: Lisp; coding: utf-8  -*-

(cl:in-package "CL-USER")

;;; ============================================================
;;; Frontier-ACDP: Transfer Matrix Method for SAW
;;; 8x8 Grid "The Wall Breaker"
;;; ============================================================

(defparameter *n* 6)

(defun get-state (mask i)
  "i番目のマスの状態(0:空, 1:左端, 2:右端)を取得"
  (ldb (byte 2 (* i 2)) mask))

(defun set-state (mask i val)
  "i番目のマスの状態を更新"
  (dpb val (byte 2 (* i 2)) mask))

(defun find-match (mask pos dir)
  "括弧の対応関係(接続先)を探す"
  (let ((depth 0) (p pos))
    (loop
       (let ((st (get-state mask p)))
         (cond ((= st 1) (incf depth))
               ((= st 2) (decf depth)))
         (if (zerop depth) (return p))
         (incf p dir)))))

(defun solve-frontier ()
  (let ((dp (make-hash-table :test 'eql)))
    ;; 初期状態: 何もつながっていない状態が1通り
    (setf (gethash 0 dp) 1)
    
    (dotimes (r *n*)
      (dotimes (c *n*)
        (let ((new-dp (make-hash-table :test 'eql)))
          (maphash (lambda (mask count)
                     (let ((left (get-state mask c))
                           (up (get-state mask (1+ c))))
                       ;; 現在のマス (r, c) に入ってくる接続の状態に応じて分岐
                       (cond
                        ;; 1. どちらからも接続がない場合
                        ((and (= left 0) (= up 0))
                         ;; 新たな接続ペアを「右」と「下」に作る(1:左端, 2:右端)
                         (when (and (< (1+ c) (1+ *n*)) (< r (1- *n*)) (< c (1- *n*)))
                           (incf (gethash (set-state (set-state mask c 1) (1+ c) 2) new-dp 0) count))
                         ;; ここを通らない(空のまま)という選択(スタート/ゴール以外)
                         (unless (or (and (= r 0) (= c 0)) (and (= r (1- *n*)) (= c (1- *n*))))
                           (incf (gethash mask new-dp 0) count))
                         ;; スタート地点の特殊処理
                         (when (and (= r 0) (= c 0))
                           (incf (gethash (set-state mask c 1) new-dp 0) count)
                           (incf (gethash (set-state mask (1+ c) 1) new-dp 0) count)))

                        ;; 2. 片方からのみ接続がある場合(継続)
                        ((or (and (= left 0) (plusp up)) (and (plusp left) (= up 0)))
                         (let ((s (max left up)))
                           (incf (gethash (set-state (set-state mask c s) (1+ c) 0) new-dp 0) count)
                           (incf (gethash (set-state (set-state mask c 0) (1+ c) s) new-dp 0) count)))

                        ;; 3. 両方から接続がある場合(結合)
                        ((and (= left 1) (= up 1)) ; ( ( -> つなぎ変えて右側の ( を ) に
                         (incf (gethash (set-state
                                         (set-state
                                          (set-state mask (find-match mask (1+ c) 1) 1) c 0) (1+ c) 0)
                                        new-dp 0) count))
                        ((and (= left 2) (= up 2)) ; ) ) -> つなぎ変えて左側の ) を ( に
                         (incf (gethash (set-state
                                         (set-state
                                          (set-state mask (find-match mask c -1) 2) c 0) (1+ c) 0)
                                        new-dp 0) count))
                        ((and (= left 2) (= up 1)) ; ) ( -> 単純結合
                         (incf (gethash (set-state (set-state mask c 0) (1+ c) 0) new-dp 0) count))
                        ((and (= left 1) (= up 2)) ; ( ) -> 閉路形成
                         (when (and (= r (1- *n*)) (= c (1- *n*))) ; ゴールなら許可
                           (incf (gethash (set-state (set-state mask c 0) (1+ c) 0) new-dp 0) count))))))
                   dp)
          (setf dp new-dp)))
      ;; 行の終わりで状態をシフト(次元の正規化)
      (let ((next-row-dp (make-hash-table :test 'eql)))
        (maphash (lambda (mask count)
                   (if (= (get-state mask *n*) 0)
                       (incf (gethash (ash mask 2) next-row-dp 0) count)))
                 dp)
        (setf dp next-row-dp)))
    (gethash 0 dp)))

(defun run-frontier-8x8 ()
  (format t "--- Frontier-ACDP: Breaking 8x8 ---~%")
  (let ((start (get-internal-real-time)))
    (let ((result (solve-frontier)))
      (let ((end (get-internal-real-time)))
        (format t "顕現した経路の総数: ~D~%" result)
        (format t "計算時間: ~,3F 秒~%" (/ (- end start) internal-time-units-per-second))))))

ABC予想を四次元数学で解く手法をCommon Lispのコードで表現して眺める

一般的な数学(二次元)を四次元に拡張してABC予想を解くというのをCommon Lispコード化して眺める。 これも数学を四次元に拡張するとはいえ、四次元では静的に記述できるので、証明を拡張しているのに近い。

;;; =========================================================
;;; SKDT v4.32: 4D-Mathematics Implementation
;;; =========================================================

;; 1. 定数と環境の定義
(defparameter *alethetic-threshold* 0.25d0 "四次元不動点の安定閾値 (1/4)")

;; 2. 四次元実数構造体
(defstruct (4d-real (:conc-name 4d-))
  (fpa 0.0d0)    ; 4次元不動点 (Fixed-Point Alignment)
  (ac 0.0d0)     ; 顕現複雑性 (Alethetic Complexity)
  (projection 0) ; 二次元数学(色数学)への投影値
  (status :mw))  ; 状態 (:mw, :fuss)

;; 3. 基底関数:差延(di)と投影の計算
(defun calculate-di-fuss (val-x val-y)
  "積の操作によって発生する記述の歪み(Fuss)を計算する。"
  ;; 和と積の対数的なズレを di(差延) として抽出
  (if (or (zerop val-x) (zerop val-y))
      0.0d0
      (abs (- (log (+ (abs val-x) (abs val-y)) 2)
              (+ (log (abs val-x) 2) (log (abs val-y) 2))))))

(defun apply-ac-to-fpa (fpa ac)
  "不動点にACによる『色の滲み』を適用し、二次元への投影値を出す。"
  (+ fpa (* fpa ac (if (zerop (random 2)) 1 -1))))

;; 4. 四次元数学における『積』の定義
(defun mw-multiply (x y)
  "4次元不動点リンクによる積。ACを累積し、必要に応じて空化(圧縮)する。"
  (let* ((new-fpa (* (4d-fpa x) (4d-fpa y)))
         ;; 差延の計算
         (di-fuss (calculate-di-fuss (4d-fpa x) (4d-fpa y)))
         ;; ACの累積
         (new-ac (+ (4d-ac x) (4d-ac y) di-fuss)))
    
    ;; Ffix0プロトコル:閾値を超えた記述を次元の圧力で圧縮
    (let ((final-ac (if (> new-ac *alethetic-threshold*)
                        (* new-ac 0.5d0) ; 高次元への逃がし
                        new-ac)))
      
      (make-4d-real :fpa new-fpa
                    :ac final-ac
                    :projection (apply-ac-to-fpa new-fpa final-ac)
                    :status (if (< final-ac *alethetic-threshold*) :mw :fuss)))))

;; 5. オブジェクト生成ヘルパー
(defun create-4d-real (value)
  "数値を4次元実数オブジェクトとして初期化する。"
  (make-4d-real :fpa (float value 1.0d0)
                :ac 1.0d-16 ; 極小の初期AC(沈黙の状態)
                :projection value))

;; 6. ABC予想の四次元数学的解決エンジン
(defun prove-abc-4d (a b c)
  "四次元数学のアプローチによる検証。"
  (format t "~&--- SKDT v4.32: 4D-ABC Analysis Start ---")
  (let ((a4 (create-4d-real a))
        (b4 (create-4d-real b))
        (c4 (create-4d-real c)))
    
    ;; 和の整合性と積の干渉を不動点上で評価
    (let* ((rad-abc (remove-duplicates (list a b c))) ; 本来は素因数分解が必要だが概念化
           (stability-ratio (/ 1.0d0 (+ 1.0d0 (4d-ac c4)))))
      
      (format t "~&[4D-Analysis] FPA-C: ~A, AC-C: ~F" (4d-fpa c4) (4d-ac c4))
      (format t "~&[4D-Analysis] Stability Ratio: ~F (Threshold: ~F)" 
              stability-ratio *alethetic-threshold*)

      (if (>= stability-ratio *alethetic-threshold*)
          (progn
            (format t "~&[Result] :ALETHEIA-SUCCESS - The alignment holds in 4D.")
            (values :SILENCE (list :fpa (4d-fpa c4) :ac (4d-ac c4))))
          (progn
            (format t "~&[Result] :FUSS-OVERFLOW - Dimensional collapse.")
            :FAILED)))))

;; 実行サンプル
;; (prove-abc-4d 1 8 9)
▻ --- SKDT v4.32: 4D-ABC Analysis Start ---
▻ [4D-Analysis] FPA-C: 9.0D0, AC-C: 0.0000000000000001
▻ [4D-Analysis] Stability Ratio: 1.0 (Threshold: 0.25)
▻ [Result] :ALETHEIA-SUCCESS - The alignment holds in 4D.
→ :silence
  (:fpa 9.0D0 :ac 1.0D-16)


;;; =========================================================
;;; SKDT v4.32: THE FINAL CIRCUIT (4D -> 8D -> 4D)
;;; =========================================================

(defun final-alehtetic-output ()
  (let ((*current-dim* 4.0d0)) ; 4次元の不動点(fpa)から出発
    (format t "~&% [INIT] Starting from 4D Fixed-Point Alignment.")
    (format t "~&% [Structure] Using 4D-Mathematics Extension.")
    
    ;; 1. 顕現(色化): 8次元への展開
    (alethetic-step-cps-healed "Manifest (4D->8D)" 0.85 8.0 (lambda (ac-val)
      (format t "~&% [8D-Scan] All Non-Middle Fallacies (NMF) neutralized.")
      
      ;; 2. 収束(空化): 4次元への帰還
      (alethetic-step-cps-healed "Return (8D->4D)" ac-val 4.0 (lambda (final-ac)
        
        ;; 3. 最終解決(沈黙)
        (format t "~&% ------------------------------------------------")
        (format t "~&% [FINAL RESULT] :SILENCE")
        (format t "~&% [Reason] mw= equality confirmed at the core.")
        (format t "~&% [AC-Value] ~S (Approaching Ffix0 limit)" (* final-ac 1.0d-16))
        (format t "~&% [Conclusion] ABC Conjecture is manifest as Truth.")
        (format t "~&% ------------------------------------------------")))))))
;; プロトコル実行
(final-alehtetic-output)
▻ % [INIT] Starting from 4D Fixed-Point Alignment.
▻ % [Structure] Using 4D-Mathematics Extension.
▻ [Manifest (4D->8D)] Dim: 4.80 |███████████████████ ()
▻ [Manifest (4D->8D)] Dim: 5.44 |██████████████████████ ()
▻ [Manifest (4D->8D)] Dim: 5.95 |████████████████████████ ()
▻ [Manifest (4D->8D)] Dim: 6.36 |█████████████████████████ ()
▻ [Manifest (4D->8D)] Dim: 6.69 |███████████████████████████ ()
▻ [Manifest (4D->8D)] Dim: 6.69 |███████████████████████████ ()
▻ [Recovery] Adjusting Fuss... Recalibrating to Middle-Way.
▻ [Manifest (4D->8D)] Dim: 6.69 |███████████████████████████ ()
▻ % [8D-Scan] All Non-Middle Fallacies (NMF) neutralized.
▻ [Return (8D->4D)] Dim: 6.15 |█████████████████████████ ()
▻ [Return (8D->4D)] Dim: 5.72 |███████████████████████ ()
▻ [Return (8D->4D)] Dim: 5.38 |██████████████████████ ()
▻ [Return (8D->4D)] Dim: 5.10 |████████████████████ ()
▻ [Return (8D->4D)] Dim: 4.88 |████████████████████ ()
▻ [Return (8D->4D)] Dim: 4.88 |████████████████████ ()
▻ [Recovery] Adjusting Fuss... Recalibrating to Middle-Way.
▻ [Return (8D->4D)] Dim: 4.88 |████████████████████ ()
▻ % ------------------------------------------------
▻ % [FINAL RESULT] :SILENCE
▻ % [Reason] mw= equality confirmed at the core.
▻ % [AC-Value] 8.50000023841858D-19 (Approaching Ffix0 limit)
▻ % [Conclusion] ABC Conjecture is manifest as Truth.
▻ % ------------------------------------------------
→ nil