# 固定命题形式证明：找证明并交给内核核验

工作单元：W-M01；版本：2026-10-21.workunits.2；复核：2026-10-20
为一个不允许偷偷改写的形式命题交付可检查证明。

## 当前用法
可委派AI搜索证明；固定命题在指定环境通过内核与公理检查后，接收这一份证明。
依据：AlphaProof Nexus公开研究展示在开放问题上搜索并交付Lean证明；Lean官方提供核验方法。它支持以证明文件为交付，不要求先相信模型解释。
来源状态：active
本站记录：本站固定实数命题的参考与替代证明已在Lean 4.19.0和固定Mathlib实际编译，额外命令、错证明、改命题等控制被拒；属于受限语法的验收器校准，新增AI试次为0。

条件：
- 形式陈述已锁定且语义经核对
- 依赖可安装并精确固定
- 可独立检查公理与完整性

## 请求与范围
研究者、学生或工程师已经锁定目标命题和允许依赖。
证明搜索可自动循环；自然语言题意到形式陈述另行核对。内核通过只接受这一命题与依赖下的证明。

## 输入
- 固定命题：可信文件中的类型、量词、定义和假设；明确允许修改的proof区域。
- 核验环境：Lean、Mathlib与依赖revision；允许公理清单和资源预算。

## 交付物
- 证明文件与使用的依赖
- 指定环境的检查日志和公理依赖记录
- 未解决子目标或搜索停止原因

## 验收
1. 证明的是原命题
   方法：比较可信声明与提交声明，核对自然语言含义
   拒收：把任意实数改成非负数，得到较弱命题再宣布通过。
2. 全部目标由允许的基础证明
   方法：干净环境内核检查并审计传递公理，拒绝sorryAx或未批准公理
   拒收：依赖文件藏有sorry，或添加axiom False。
3. 可重复核验
   方法：保留版本与命令；合理不同证明也应被接受
   拒收：只给截图或模型说“编译成功”，没有可检查文件。


## 具体例子
输入：固定实数x、y，目标2*x*y ≤ x^2+y^2；不增加x或y非负条件。
预期产物：基于(x-y)^2≥0的证明文件、核验日志和依赖列表。
失败：改证0≤x^2+y^2，或用sorry占位，却把编译输出当完整证明。

限定校准样例（不代表当前代表例的AI运行）：/work-unit-examples/math

## 工作重组
以前：人寻找引理并写证明，再由同行逐段检查。
现在：人锁定问题和允许假设；AI搜索、调用Lean、根据反馈修订；机器检查形式正确，人核对题意与意义。
保留：
- 形式陈述与原问题一致
- 允许公理和研究贡献判断
新增：
- 维护可搜索的形式库
- 检查证明依赖与版本
- 记录未成功搜索

## 人的责任与失败接管
明确问题及可接受假设，核对形式语义和结果意义；证明步骤可由AI产生，内核承担精确逻辑检查。
预算结束但仍有目标时交出已证引理、未解目标和尝试范围；不能加假设或把未找到证明说成命题为假。

## 尚待补足
- 当前只校准固定命题的受限证明语法；新领域题型和更完整语法需独立验收与隔离运行。
- 对目标领域的未见命题记录搜索预算与失败，不用成功案例推普遍覆盖

## 职业与团队下一步
形式化数学、验证工程、AI数学研究支持
展示固定声明、证明文件、内核日志和自然语言对照，并解释一个被拒的弱化命题。
区分研究数学岗位与形式验证工程岗位，核对所需理论背景和编程能力；先补实际证明资产再选方向。
/explore?purpose=career&domain=math
瓶颈是找证明、形式化基础库，还是核对原意？
把可锁定目标交给搜索Agent；让数学人员审题意，验证工程人员维护依赖与检查。
试点一组不同来源的引理，统计发现、形式化和检查各自成本，再决定投入工具、培养或招专门人员。
/explore?purpose=team&domain=math

## 证据与关系
- AlphaProof Nexus：形式证明搜索进入开放数学问题：https://arxiv.org/html/2605.22763v1
  定位：摘要、§2输入输出、§5与§6、附录A.1/B.2；公开 2026-05-21；核查 2026-10-19；复查 2026-10-26
  支持：完整搜索与形式反馈的作者报告。；已有完整产物支持限定委派。
  未覆盖：不是本站实数不等式或任意新命题的概率。；不继承本站验收器校准为AI能力。
- Lean官方：怎样验证一份证明：https://lean-lang.org/doc/reference/latest/ValidatingProofs/
  定位：检查形式陈述、内核与公理依赖相关章节；公开 未标注（持续更新文档）；核查 2026-10-19；复查 2026-10-26
  支持：独立形式检查方法。
  未覆盖：文档不提供模型找证明成功率。


## 任务级判断与证据
采用方式：限定条件下整包委派
从证据到建议：Nexus等外部研究表明搜索可以交付完整证明；内核允许对交付逐份接收而不先假定可靠性。本站受限命题仅校准验收器，不是找证明能力样本；新领域仍需固定声明和依赖。
当前可用性：mixed；旧本站样例为Lean4.19.0固定Mathlib的受限校准；新的证明任务须重新固定项目，公开工具可调用不等于本题已跑。
- Lean核验：https://lean-lang.org/doc/reference/latest/ValidatingProofs/
  历史样例Lean4.19.0；新任务按项目锁定；开源工具；实际构建与依赖审计按任务运行。
- Aristotle：https://pypi.org/project/aristotlelib/2.1.0/
  aristotlelib2.1.0；需账号/API key，本站未调用。

### 外部研究已交付固定形式问题的证明文件，允许按产物而非生成解释接收。
依据身份：外部报告结果；状态：active
- AlphaProof Nexus：形式证明搜索进入开放数学问题：https://arxiv.org/html/2605.22763v1
  定位：§2/§3 Table1、Failure Analysis；关系：partial
  支持：完整搜索与形式反馈的作者报告。
  限制：不是本站实数不等式或任意新命题的概率。
  核查：2026-10-19；来源状态：active
配置：Nexus v1；Gemini3.1Pro基础代理，完整配置含进化搜索/AlphaProof；题集/预算限定，成功后专家核对题意。
适用限制：不是本站实数不等式或任意新命题的概率。
相关进展（本条判断）：
- 证明搜索开始在开放问题上交付可检查结果：/explore?purpose=understand&domain=math&window=all#P-M-NEXUS
  首次公开 2026-05-21；判断变化 2026-05-21

### 固定命题的接受须同时核对可信声明、内核和传递公理。
依据身份：工具与方法依据；状态：active
- Lean官方：怎样验证一份证明：https://lean-lang.org/doc/reference/latest/ValidatingProofs/
  定位：Printing Axioms / Gold Standard；关系：method
  支持：独立形式检查方法。
  限制：文档不提供模型找证明成功率。
  核查：2026-10-19；来源状态：active
适用限制：文档不提供模型找证明成功率。

### 当声明、环境和允许依赖已固定，可整包委派证明搜索并逐份独立接收；未完成只交实际进展。
依据身份：有条件的编辑推断；状态：active
- AlphaProof Nexus：形式证明搜索进入开放数学问题：https://arxiv.org/html/2605.22763v1
  定位：§3 Failure Analysis；结果仓库；关系：adjacent
  支持：已有完整产物支持限定委派。
  限制：不继承本站验收器校准为AI能力。
  核查：2026-10-19；来源状态：active
适用限制：不继承本站验收器校准为AI能力。

## 情境变化
### 固定研究引理
输入变化：换为领域特定形式声明，proof区以外不变。
判断变化：可搜索；成本和适用库需重新核实。
验收变化：完整项目重建、可信声明对照及公理检查。
### 尚未形式化的题意
输入变化：只有自然语言目标。
判断变化：先用W-M05交付语义对照，不把类型可编译视为已证明原题。
验收变化：先接收形式声明，再验对应证明。

研究前沿：内部研究配置已在特定开放问题交付文件；公开证明服务有入口，但不能继承研究配置的预算和覆盖。
下一项验证：对一组未泄漏、目标不变的领域引理运行公开工具，保存预算与失败；先确保正确替代、弱化命题及隐藏未证依赖分别被接收/拒绝。
未来改判信号：
- 扩大：未见命题在固定声明下完整证明并通过依赖审计，重试/成本可追踪。
- 收缩：成功依赖改题、sorry或不允许公理；将交付降为未解目标与部分引理。

## 与本单元直接关联的进展
### 证明搜索开始在开放问题上交付可检查结果
公开 2026-05-21；判断变化 2026-05-21
Nexus研究配置把证明、反例及对象/参数探索接到形式反馈；公开的是成果集合。
支持范围：原论文问题集和成功选择有边界；事后九题比较不能当新问题概率；本站未重放，公开结果仓库不是Nexus API。
来源状态：active
/explore?purpose=understand&domain=math&window=all&kind=all#P-M-NEXUS

领域背景与未来情景：/explore?purpose=understand&domain=math


## 工具与采用佐证
### Lean/Mathlib：证明交付有可执行的检查基础
来源状态：active
核查层级：implementation_inspected；日期：2026-10-19；版本：e3e75e86143b43849829fdcd44a39a6b0fe35234
原始主张：数学库提供定理、策略、工具链与构建流程。
已检查：已核对固定commit README、lean-toolchain、依赖清单及CI配置；最新主分支标为Lean 4.36.0-rc1。本站代表契约另固定Lean 4.19.0并已编译校准。
支持：形式证明可以把接收条件落实为固定命题的内核检查和公理核对。
限制：最新主分支检查与本站旧固定版本重放不是同一次运行；库规模不等于AI证明能力。
下一步：工具链升级后用相同锁定命题、参考解、额外公理和命题替换反例重跑；再增加新题型，保留语义人工核对。
https://github.com/leanprover-community/mathlib4/blob/e3e75e86143b43849829fdcd44a39a6b0fe35234/README.md

### Aristotle：形式证明从研究成果走向工具接口
来源状态：active
核查层级：claim_checked；日期：2026-10-19；版本：product-page-observed-2026-10-19
原始主张：产品页声明从英文问题或现有Lean项目开始证明与形式化，并可产生库可用代码。
已检查：已读官方产品页能力声明；未调用服务。
支持：证明工作已经有面向使用者的产品候选，可以用本站锁命题与公理验收方案核查其输出。
限制：产品承诺、推荐语和“数学超级智能”措辞不替代任务结果；自然语言与形式命题可能不一致。
下一步：在已获服务授权和预算后提交锁定命题与已知假命题，下载实际证明，离线内核检查并核对语义、版本、失败和人工修改。
https://aristotle.harmonic.fun/