数学界筹备新期刊：要求论文证明经 Lean 形式化验证

多位数学家正筹备创办一本新期刊，除开放获取等传统价值外，明确两项核心原则：更看重论文对理解结果的深化而非抢先发表首个证明；论文须在 Lean 中完成证明的形式化验证方可录用。发起者指出，随着 LLM 越来越多用于数学证明，细微难查的错误风险上升，因此需要形式化验证把关。他们同时借 Terry 的博客征集反馈，并欢迎关于未来期刊不同定位与做法的讨论。