有人用 LLM 辅助在 Lean 里写 Zstandard 解压器与证明 RSS

个人实验，没有给出可推广的成功率，产出仍需 proof checker、测试与人工审阅把关。