We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, set cover, center selection, load balancing, and bin packing. We uncover incompletenesses in existing proofs and improve the approximation ratio in one case. All proofs are uniformly invariant based.

翻译：我们首次正式核实了NP-完全优化问题的近似算法:顶点覆盖、独立设置、设置覆盖、中心选择、负载平衡和垃圾包装。 我们发现现有证据的不完善之处,并改进了一个案例中的近似比。 所有证据都以不变为基础。