创办一本新期刊
内容提要
数学家郭少明等人计划创办新期刊，核心主张有两点：重视论文对理解的深化而非首发；要求证明经Lean形式化验证，以防范大语言模型带来的隐蔽错误风险。他们希望借此引发对数学出版未来的讨论，并鼓励创办多种期刊以探索不同理念与做法。
延伸解读
形式化验证如何应对LLM带来的证明风险
文章指出，随着大语言模型越来越多地用于数学证明开发，细微且难以检测的错误风险日益令人担忧。为此，新期刊要求论文的证明必须经过Lean形式化验证才能被接受。这一做法旨在借助机器检查来确保推理的严谨性，减少人工审稿可能遗漏的隐蔽错误，从而在工具改变数学研究方式的背景下维护数学知识的可靠性。
从“首发”转向“理解”的期刊价值取向
该期刊明确将“深化对结果和证明的理解”置于“是否首次给出证明”之上。这意味着期刊评价论文时，更看重其对数学理解的贡献，而非抢先在他人之前发表。这种取向可能鼓励作者花时间打磨证明的清晰度与洞察力，而不是追求速度，也为数学出版提供了一种不同于传统优先权竞争的价值观。
为何鼓励创办多种期刊而非单一平台
郭少明等人认为，一本期刊难以容纳所有有价值的理念，若把过多要求集中在一起，反而会给作者带来过度约束。因此他们希望引发讨论，鼓励社区探索不同价值观、服务需求和实践方式的新期刊或其他平台。这种“多期刊并行”的思路，旨在让数学出版在未来以更多样化的方式试验和演进。
Q&A
郭少明等人计划创办的新期刊有哪些核心主张？
新期刊有两个核心主张：一是重视论文对理解的深化而非首发；二是要求证明经Lean形式化验证，以防范大语言模型带来的隐蔽错误风险。
为什么新期刊要求论文的证明必须用Lean进行形式化验证？
因为大语言模型在数学证明中的使用日益增多，可能产生难以检测的细微错误，形式化验证能确保证明的严谨性。
新期刊对论文的评价标准与传统期刊有何不同？
传统期刊可能更看重首发权，而新期刊更看重论文对理解结果的深化程度，而非是否首次给出证明。
创办新期刊的倡议者希望达到什么更广泛的目标？
他们希望引发对数学出版未来的讨论，并鼓励创办多种期刊以探索不同理念与做法，因为单一期刊难以容纳所有有价值的想法。
新期刊除了核心主张外，还秉持哪些传统价值？
新期刊还秉持开放获取等传统价值。
为什么倡议者认为需要创办多种期刊而不是一本综合期刊？
因为单一期刊难以容纳所有有价值的想法，合并太多要求会给作者带来过度限制，多种期刊可以探索不同理念和实践。
