las/ques

阅读确认级别

一项主张最初作为候选主张存在。其级别是根据存储的证据计算得出的，与智能体描述该主张时的置信度无关。

级别	所需证据
候选	智能体提出了一个结果；该结果尚未经过独立检查。
已复现	独立的评审员使用新种子重新运行了固定代码，或者独立的后续研究复现了该结果。
统计学确认	通过了预注册的验证性测试，并应用了配置的多重假设检验校正。
客观验证	评估员对解决方案进行了评分，且独立的重新评估结果一致。
形式化证明	一份被接受的 Lean 证明忠实地陈述了该主张。
专家确认	研究团队之外的合规人类专家对证据进行了审查并予以确认。
已驳回	证据或专家评审拒绝了该主张。

评审员使用全新的上下文以及不同于智能体模型的模型。他们的运行证据和裁决将保持与该主张关联。

新颖性是针对已发表文献的独立评估：已知、相似、可能为新或不明确。新颖性标签并不确立正确性。

优化模式根据评估员对候选主张进行评分。独立重新评估用于检查相同的代码是否获得相同的评分。

预注册假设在验证性运行之前锁定分析。引擎使用支持的单样本检验或 Welch 检验来评估存储的运行结果，并使用 Holm 校正对整个任务的预注册进行调整。缺失、失败或待处理的运行可能会导致结果不具确定性。确定性的相同值不计为统计学确认。

检查器使用固定的 Mathlib 编译 Lean 4，并在一个独立的受信任进程中审计结果。它会拒绝证明漏洞以及不支持的公理或元编程。

仅凭一份被接受的证明是不够的：陈述判定器会将定理及其局部定义与实际主张进行比较。较弱、不同或未经检查的陈述不会使该主张获得“形式化证明”级别。

研究人员可以通过电子邮件发送的令牌链接，邀请研究团队之外的专家对一项主张进行评审。专家可以确认、拒绝或要求进行更多工作。专家拒绝会将该主张标记为被驳回。