内部测试：编辑代作者提交。支持单个 Lean 4 文件及 PDF；每次提交形成独立记录。机器检查与论文对应性审核分别呈现。
环境由验证员固定。暂不接受 ZIP、自定义依赖和构建脚本。环境不兼容会单独记录。