FormalizeSampling：用 Lean 4 机器验证采样与扩散模型收敛定理

Hendry Dong 发布并开源 FormalizeSampling 项目，用 Lean 4 与 Mathlib 形式化采样算法和扩散模型的已发表收敛定理。项目连接 Langevin 动力学、近端采样与扩散模型，提供端到端收敛证明、解析反例及路径收敛与输出收敛的分离结果；图中 LSI 衰减定理示例已在 Lean 4.35.0 下通过 #print axioms 检查。