研究プロジェクトにおいて、関数型プログラミング言語および対話型定理証明機であるLean 4を用い、整数乗算が最悪計算量O(n (log n)^(1-κ))で実行可能であることを示す証明の形式化に成功しました。この文脈において、「n」は符号化された入力の総長を表し、「κ」（kappa）は標準的なO(n log n)の複雑度に対する指数的な節約を表します。GitHub上で`integer-mult-bounds-lean`として公開されているこのプロジェクトは、標準的なバイナリ符号化を用いてすべての自然数のペアを乗算する固定マルチテープ・チューリングマシンの形式的検証を提供しています。
この特定の構成は、約0.0000468908（または2^-14.38）のkappa値を達成しています。この結果は、過去の歴史的な境界に対して測定可能な改善を意味するため重要です。そのメカニズムには、T16ノード上での「丸められた合成レイヤー（rounded synthetic layers）」と「コンパクトな制御（compact controls）」の複雑なアーキテクチャが含まれています。この証明には、入力の準備と配布から、最終的な変換、出力、およびクリーンアップに至るまでの操作の全パイプラインが含まれています。Lean 4を使用することで、研究者たちは証明が数学的に健全であること、および、有限の状態とスキャンされた記号のみを認識するマシンの遷移関数が定義された意味論に厳密に従っていることを保証しています。
現在のkappa値は一つの節目ではありますが、プロジェクトは無条件のkappa値0.0023という長期目標に向けて進んでいます。これには「Design-B」コンパイラと有限の混合から一様へのコンパイラの統合が含まれます。現在、「Design-B」コンパイラは進行中であり、現在の結果よりも約28%高い、約0.0000600の節約を提供すると予測されています。また、このプロジェクトは「ネイティブマシン」ターゲットも維持しており、これは固定されたアルファベットと一次元のテープを持つ決定論的マシンですが、その現在の指数節約は、主要な改善ルートとして追求されている現在のMathlibの結果よりも小さくなっています。