准确说明检查范围
有限计算只对所列输入和检查范围成立。大量例子中的规律可以启发猜想,但不能证明关于无限情形的命题。证明需要列明假设,并覆盖命题量词所要求的全部情况。
本档案分别记录数学状态、形式化验证和评审状态。取得有用的中间结果,不代表原来的开放问题已经解决。论证是否成立与结果是否具有新颖性,也需要分别判断。
形式化验证
存在 Lean 源文件,并不意味着整个项目都已获得形式化认证。每项成果应注明准确的定理、检查所用工具链、假设,以及形式化开发覆盖的论证范围。未被该开发覆盖的计算需要单独说明和核查。
AI 辅助与评审
AI 工具用于探索思路、编写和检查代码、草拟论证以及翻译页面。不同智能体进行的检查仍属于内部检查。只有在有明确记录表明外部人员检查了指定版本时,才使用外部评审的说法。同行评审必须对应实际的学术出版评审程序。
英文概览页是编辑原稿。德文和中文采用 AI 辅助翻译,并标注为待语言审校。讨论科学命题时,应查阅准确的原始版本,不能只依据翻译摘要。
版本与更正
公开版本应将正文、证据、文件和修改说明关联起来。后续更正生成新版本,旧版本仍可引用。如果需要撤回某个版本,其状态和原因应继续显示。
文件出现在工作目录中,不等于它已获准公开。发布手稿或研究下载前,需要明确检查其内容、假设、署名和支持材料。