AI 中文总结
该研究证明随机3-SAT公式的可满足性阈值上界为4.268，基于插值与能量方法，通过与简单约束系统比较简化为有限计算，在Lean 4中形式化，使严格上界接近腔方法预测值。
AI 中文摘要
我们证明，具有n个变量和⌊4.268n⌋个子句的随机3-SAT公式，以高概率是不可满足的。可满足性阈值已受到大量关注：Díaz、Kirousis、Mitsche和Pérez-Giménez的工作中，相继的上界达到了4.4898，而腔方法预测该值接近4.267。我们的上界使严格的上估计值接近这一预测。该证明基于早期的插值方法，包括Achlioptas和Menchaca-Méndez的能量方法。我们研究任意赋值必须违反的最小子句数，将随机公式与关于单个变量的更简单约束系统进行比较。这种比较将上界简化为有限计算，我们使用精确有理算术验证了该计算。该证明在Lean 4中形式化。
英文摘要
We prove that a random 3-SAT formula with $n$ variables and $\lfloor 4.268n\rfloor$ clauses is unsatisfiable with high probability. The satisfiability threshold has attracted considerable attention: successive upper bounds reached 4.4898 in the work of Díaz, Kirousis, Mitsche, and Pérez-Giménez, while the cavity method predicts a value near 4.267. Our bound brings the rigorous upper estimate close to this prediction. The proof builds on earlier interpolation methods, including the energetic approach of Achlioptas and Menchaca-Méndez. We study the smallest number of clauses that any assignment must violate, comparing the random formula with a simpler system of constraints on individual variables. This comparison reduces the bound to a finite calculation, which we verify using exact rational arithmetic. The proof is formalized in Lean 4.
Comments16 pages, 1 figure. Includes a complete Lean 4 formalization and a reproducible rational certificate
