计算复杂度领域的一项新理论突破引入了一种最坏情况时间复杂度为 o(n log n) 的整数乘法算法。虽然通过快速傅里叶变换 (FFT) 方法实现 O(n log n) 乘法已经有一段时间了，但 o(n log n) 的结果代表了一种严格的改进，表明其复杂度严格低于标准的线性对数边界。这一进展源于近期的研究，包括 David Harvey 和 Joris van der Hoeven 的工作，他们建立了基础的 O(n log n) 结果，并为这些进一步的改进提供了框架。
为了确保这一新结果的数学完整性，开发人员目前正使用 Lean 4（一种函数式编程语言和交互式定理证明器）来形式化该算法。该项目托管在 GitHub 上，旨在提供一个无条件的证明，即固定的多带图灵机可以在 O(n * (log n)^(1-kappa)) 边界内执行乘法。目前的形式化已实现了 kappa approx 2^(-14.38) 的正向节省。该实现涉及一种复杂的架构，结合了线性直接中国剩余定理 (CRT) 路由、紧凑控制和全宽块。通过使用 Lean，研究人员可以验证机器的转换函数和由此产生的复杂度边界在数学上是正确的，而无需依赖未经批准的公理或承认的证明。
尽管在形式化方面取得了进展，但仍存在某些技术障碍。虽然目前的证明对于 2^(-14.38) 的节省已经完成，但该项目的最终目标是获得更强的指数节省 83/10^12。此外，当前结果并不能直接转化为固定有限域（如 F_2[x]）上多项式乘法的新复杂度边界，后者在计算复杂度中仍是一个独立的问题。形式化过程还需要大量的计算资源；该项目利用受保护的构建脚本来管理内存限制和执行时间，突显了在形式化环境中验证此类高水平数学证明的强度。