一个研究项目已成功在 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 节点上复杂的“舍入合成层”和“紧凑控制”架构。该证明包含了操作的整个流水线，从输入准备和分布到最终的变换、输出和清理。通过使用 Lean 4，研究人员确保了证明在数学上是严谨的，并且机器的转换函数（仅能看到有限状态和扫描到的符号）严格遵守定义的语义。
虽然当前的 kappa 值是一个里程碑，但该项目正朝着 0.0023 的无条件 kappa 的长期目标迈进。这将涉及集成“Design-B”编译器和有限混合到统一编译器。目前，“Design-B”编译器正在开发中，预计将提供约 0.0000600 的节省，比当前结果高出约 28%。该项目还维护一个“原生机器”目标，这是一个具有固定字母表和一维带子的确定性机器，尽管其当前的指数节省小于为主要改进路线追求的活跃 Mathlib 结果。