Ground False / ProofNet-Verified 获 NeurIPS 2026 E&D Track 接收，揭示 formal-math benchmark 的 ground truth 也可能大规模失真

作者 9 月 24 日确认 Ground False 被 NeurIPS 2026 E&D Track 接收。其公开 ProofNet-Verified 审计显示：在 367 个 ProofNet 问题中，原 ProofNet 有 204 个问题存在错误或歧义，ProofNet# 仍有 97 个；其中大量问题来自 informal-to-formal 语义不忠实、缺失前提以及对 Lean/Mathlib 的误解。项目不仅标记错误，还通过证明错误形式化的否定、给出 trivializing proofs 或详细语义分析来确认问题，并发布修正后的 Lean 4 statements 与 proofs。