像把八件小物品塞进一个盒子里一起称重，INT4点积也想把八个4位整数装进一个32位寄存器，同时完成乘加。这样，缺少原生向量指令的WebAssembly或旧款ARM也能获得部分并行能力。难点是数值太窄，拆包、符号处理和累加很容易在边界处出错。
作者没有手写这套位运算，而是让Z3——一种自动求解逻辑约束的工具——从AND、移位和乘法等指令中搜索公式。候选方案若在随机测试中失败，反例就会送回Z3继续约束搜索。最终得到的无分支序列利用32位乘法，让寄存器两端的两组4位乘法同时发生且互不干扰。随后，作者把函数移植到Lean 4定理证明器，希望覆盖两个32位输入对应的全部2^64种组合，而不只是一百万次随机测试。供稿在Lean 4证明过程处截断，因此尚无法判断证明脚本、性能数据及复现情况。