# 数学研究产物：联合探索命题、构造与证明或反例

工作单元：W-M04；版本：2026-10-21.workunits.2；复核：2026-10-20
围绕一个研究问题交付语义一致的结论及可核验论证/构造/反例，或明确已解决部分与未解障碍。

## 当前用法
可把问题族探索与候选研究产物整包交给AI；按约定产物分别接收。已有公开个案证明研究循环可产生完整成果，任意新问题的完成概率与公开工具复现能力仍待核。
依据：Nexus作者报告联合搜索参数与证明，并有Erdős125固定证明产物；不是把W-M01固定形式命题的受限本地校准外推到研究。
来源状态：active
本站记录：本站M04模型运行数、成功率、成本及人工时间均为null；只读过Erdős125公开证明文本，未独立构建，不继承W-M01本地控制通过。

条件：
- 原题和可调对象边界可核对
- 产物有独立验收途径
- 研究系统与实际可调用工具身份分开

## 请求与范围
研究者有问题方向或参数化对象，尚未锁定最终构造与证明；需要探索能成立的结论及失败边界。
允许在约定空间联合搜索对象、算法/构造参数、辅助命题与证明；不可偷偷改变原问题的对象域、量词和目标。自然语言论证、精确反例、形式证明有不同接收条件；新颖性另核对，不强制全部产物先转Lean。

## 输入
- 问题与题意对照：原始问题和来源、对象域、量词、边界定义及已知结果；哪些是本题/变体、哪些目标不可改变。已有成果复现与新研究分开标记。
- 可调对象及目标：允许改动的构造、参数域、待优化界/常数与约束；若只可搜索辅助引理，明确禁止把反例不存在的假设加进原题。
- 交付类型和研究环境：约定自然论证/反例/形式证明中的可接受结果，精确计算工具及版本；形式任务固定Lean/Mathlib和公理；检索范围、预算与停止条件，成本未知不假定可重现。

## 交付物
- 问题定义与自然语言/符号声明对照，列出原题、变体、已知成果、新猜想和未决歧义
- 最终对象/参数/构造及性质保证成对交付；包含精确证书或证明、引理依赖、计算程序与复现命令（按产物适用）
- 研究记录：关键路线、被反例排除的范围、尚未解的具体目标；不是固定逐步操作日志
- 可读研究说明、公开来源定位及贡献/修订记录；形式成果另附项目锁定文件、构建/公理核查输出

## 验收
1. 先确认研究的就是原问题或明示变体
   方法：独立核对对象域、量词、下/上/自然密度或其它关键定义与原文；列题意对照，不把弱化结论当原题答案。
   拒收：把“下密度>0”换成“上密度>0”；允许空集造成平凡构造仍宣称解决要求非平凡对象的题。
2. 构造和保证相互对应
   方法：独立重算候选对象/参数，核对每项约束与最终证明覆盖；改参数后旧证明必须同步重验。
   拒收：数值搜索找到一个好参数但保证只证旧参数；浮点近似当精确反例。
3. 自然论证/反例按各自对象接收
   方法：自然证明由具备领域能力的独立接收者检查全部关键引理、边界与引用，可用工具补检但不宣称内核认证；有限反例精确重算并验证全部前提；渐近反例需无限构造和相应论证。
   拒收：有限搜索未发现反例被当证明；自然语言关键步骤循环引用；有限n上的异常被当下密度的反例。
4. 形式证明额外满足内核与语义
   方法：只对约定形式交付：固定项目干净构建、比较可信目标声明、检查传递公理拒绝sorryAx/未批准公理，并核对可读说明与实际定理覆盖。
   拒收：编译通过但依赖含sorry；形式化只覆盖支撑引理却写成主结论已证；随意增加假设。
5. 区分完成、未解决与新颖性
   方法：交付按实际覆盖标识完整结论/条件结论/反例/未解决；独立查文献与修订记录，已知成果复现不计新发现。
   拒收：预算耗尽宣布命题为假；重放公开证明标“首次解决”；撤回后仍引用原结论。


## 具体例子
输入：已有成果复现：A是三进制只含0、1的非负整数，B是四进制只含0、1的非负整数，判断A+B下渐近密度是否为正（计数比例liminf）。原命题不可改；有限计数只作探索。新研究变体可另约定改变进制/数字集，但须另立目标，不能继承原结论。
预期产物：固定公开文件在0647711a…下的target_theorem_0把该正下密度命题答案填False并给证明；交付需题意对照、可读稿、固定依赖与独立检查。本轮仅文本核对，未重放。成果入口见WU-NEXUS-125。 来源仓库将可读稿说明为沿Lean结构整理的人工稿，不当作未经整理的AI运行轨迹。
失败：观测若干有限上界下比例较小就宣布下密度为零；把正下密度换成别的密度概念；把已公开Erdős125重新标为新发现。

## 工作重组
以前：先凭经验挑构造或参数，再尝试证明；数值试验、证明草图和形式化相互交接，反馈较晚。
现在：代理可在允许的对象/参数空间尝试构造，同时寻找证明或反例；精确计算、文献或形式错误反馈可以改变辅助命题与搜索方向。路径依题而定，确定性穷举可直接运行；不规定所有数学问题都要并行或Lean。
保留：
- 原题及研究范围核对
- 结果意义/新颖性核查
- 允许依赖与资源投入
新增：
- 对象与保证成对版本化
- 自然论证和形式产物覆盖对照
- 失败范围与修订传播

## 人的责任与失败接管
研究接收者确认问题含义、允许变体、领域论证与贡献定位并承担发布责任；这些核对也可由AI协助，不写成永久能力分工。形式内核只承担指定声明的逻辑检查。
给出已证引理、候选构造、排除参数范围和最小未解目标，区分预算耗尽、环境不可用、语义冲突和真实反例；不靠sorry或新增假设伪装完成。已有材料撤回则检查其依赖的候选与说明。

## 尚待补足
- 公开服务在新问题及限定预算下的复现尚未知
- 自然论证需领域独立审阅；参数联合搜索个案不等于一般数学研究可靠性

## 职业与团队下一步
数学研究、计算/形式化数学、研究工程
展示原题、构造与保证、题意/文献差异、失败边界及适用的独立核验；已知复现清楚标识。
按目标领域选择真实问题与接收者；区分构造发现、论证正确、形式化和新颖贡献，补齐最弱的一层。
/explore?purpose=career&domain=math
瓶颈在候选对象、证明路线、形式库还是题意与文献定位？
以研究产物委派代理，自行组织检索/计算/证明；领域接收者独立核对语义及贡献，工具核查适用的精确证书。
分别做已知成果复现和未见问题探索，记录完整成本与未解决路线；不能只展示成功题。
/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
  支持：支持对象/参数与证明联合探索的研究组织，及未证引理等失败模式；支持研究循环保留语义核对和未完成出口。
  未覆盖：内部研究配置，不等于公开API；不把Erdős125说成参数优化实验；不同产物的具体接收条目是编辑设计。
- Nexus Erdős125：固定公开证明产物：https://github.com/google-deepmind/alphaproof-nexus-results/blob/0647711a71183c1ea492ad60860776617ce1ea88/APNOutputs/ErdosProblems/erdos_125.variants.positive_lower_density.lean
  定位：L42-L54定义；L342-L370 target_theorem_0；同提交 NaturalLanguageProofs/ErdosProblems/erdos125.pdf、lean-toolchain及lake-manifest.json；公开 2026-06-05（固定提交）；核查 2026-10-20；复查 2026-11-03
  支持：给出本代表例可检查的对象和目标定理入口；区分研究结果集合与可运行代理。
  未覆盖：只查文本；尚未本站构建/独立语义裁定，不代表新研究成功率；可下载证明不等于生成系统可获得。
- Lean官方：怎样验证一份证明：https://lean-lang.org/doc/reference/latest/ValidatingProofs/
  定位：检查形式陈述、内核与公理依赖相关章节；公开 未标注（持续更新文档）；核查 2026-10-19；复查 2026-10-26
  支持：支持形式交付的公理与可信目标核对。
  未覆盖：Lean文档不认证自然语言论证或数学新颖性。
- Aristotle官方分发包2.1.0与调用入口：https://pypi.org/project/aristotlelib/2.1.0/
  定位：Quick Start / Authentication / CLI与API；服务 https://aristotle.harmonic.fun/；公开 2026-06-18；核查 2026-10-20；复查 2026-11-03
  支持：证明工具的可调用候选入口。
  未覆盖：未调用；不承诺能完成本例或复现Nexus配置。
- OpenAI公开新的数学研究产物：https://openai.com/index/sharing-ai-progress-in-mathematics/
  定位：正文结果发布、Lean材料与修订协议；10月15日资金更新；公开 2026-10-06；核查 2026-10-19；复查 2026-10-26
  支持：内部模型研究产物的直接发布及状态。
  未覆盖：不是全部开放题独立解决或公开服务稳定性。
- OpenAI十月数学公开产物固定版本与修订：https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a
  定位：README L12-L20/L40-L44；history.md L5-L31；lean/ComparatorChallenges/README.md L12-L28；公开 2026-10-06；固定提交2026-10-12；核查 2026-10-20；复查 2026-10-27
  支持：固定手稿、部分形式化、人工整理和修订入口。
  未覆盖：尚未逐稿独立重放/学术裁定。


## 任务级判断与证据
采用方式：探索与候选交付
从证据到建议：外部研究及固定产物使“仅可局部辅助”的一概判断不成立；但研究系统非公开服务，个案和选择过的问题集也不支持任意新题概率。因此可委派完整探索和候选产物，是否完成由语义、正确性、覆盖与新颖性分别接收；已知复现可直接接收可重放成果，新研究保留未解决出口。 这一发布进一步支持以具体研究产物扩大观察范围，但其内部配置、人工整理和局部形式化不能压成统一自主成功率。
当前可用性：mixed；Nexus为研究系统，开放的是结果集合；Lean项目可重建，Aristotle有公开鉴权入口。三者不合并为“现在已能复现Nexus”。本站未调用付费服务。
- Nexus固定成果仓库：https://github.com/google-deepmind/alphaproof-nexus-results/tree/0647711a71183c1ea492ad60860776617ce1ea88
  0647711a…；Lean4.27.0；lake-manifest锁定依赖；公开结果文本与项目；生成代理不作为公开产品提供。
- Lean proof validation：https://lean-lang.org/doc/reference/latest/ValidatingProofs/
  实际复现使用仓库Lean4.27.0；参考文档2026-10-20读取；开源内核/工具链；需安装固定依赖；文档latest不替代项目版本。
- Aristotle CLI/API：https://pypi.org/project/aristotlelib/2.1.0/
  aristotlelib2.1.0；需账号/API key与服务预算；本站未调用；SDK链接的GitHub源码入口此前404，不声称已核实源码。

### Nexus论文报告联合搜索算法参数与证明保证；对象设计和证明搜索可以互相反馈。
依据身份：外部报告结果；状态：active
- AlphaProof Nexus：形式证明搜索进入开放数学问题：https://arxiv.org/html/2605.22763v1
  定位：§4 Optimization Theory；§2 Agent Architecture；§3 Failure Analysis；关系：partial
  支持：支持对象/参数与证明联合探索的研究组织，及未证引理等失败模式。
  限制：内部研究配置，不等于公开API；不把Erdős125说成参数优化实验。
  核查：2026-10-19；来源状态：active
配置：arXiv2605.22763v1；完整研究代理含Gemini3.1Pro基础代理、进化搜索及AlphaProof；论文不同实验预算不同；成功个案成本不含完整选题搜索。本站未重放。
适用限制：本站未进行该任务的模型运行，不能据此给出本地成功率。
相关进展（本条判断）：
- 证明搜索开始在开放问题上交付可检查结果：/explore?purpose=understand&domain=math&window=all#P-M-NEXUS
  首次公开 2026-05-21；判断变化 2026-05-21

### Erdős125正下密度变体有固定公开Lean文件及可读稿，可将“研究成果”落到具体声明而非榜单。
依据身份：可检查产物；状态：active
- Nexus Erdős125：固定公开证明产物：https://github.com/google-deepmind/alphaproof-nexus-results/blob/0647711a71183c1ea492ad60860776617ce1ea88/APNOutputs/ErdosProblems/erdos_125.variants.positive_lower_density.lean
  定位：L42-L54定义；L342-L370 target_theorem_0；同提交自然语言PDF；关系：direct
  支持：给出本代表例可检查的对象和目标定理入口。
  限制：只查文本；尚未本站构建/独立语义裁定，不代表新研究成功率。
  核查：2026-10-20；来源状态：active
适用限制：固定公开产物存在不等于本站验收通过，已知复现不计新发现。

### 自然证明、精确反例与形式证明分别接收；形式证明还要查原声明、传递公理和语义对应。
依据身份：有条件的编辑推断；状态：active
- Lean官方：怎样验证一份证明：https://lean-lang.org/doc/reference/latest/ValidatingProofs/
  定位：Validating a Lean Proof：Printing Axioms / Gold Standard；关系：method
  支持：支持形式交付的公理与可信目标核对。
  限制：Lean文档不认证自然语言论证或数学新颖性。
  核查：2026-10-19；来源状态：active
- AlphaProof Nexus：形式证明搜索进入开放数学问题：https://arxiv.org/html/2605.22763v1
  定位：§3 Failure Analysis；§6 Discussion：semantic verification；关系：method
  支持：支持研究循环保留语义核对和未完成出口。
  限制：不同产物的具体接收条目是编辑设计。
  核查：2026-10-19；来源状态：active
适用限制：本站未进行该任务的模型运行，不能据此给出本地成功率。

### Aristotle有SDK/CLI/API的官方分发入口，可作为公开证明工具候选；Nexus结果仓库不能当作Nexus服务入口。
依据身份：工具与方法依据；状态：active
- Aristotle官方分发包2.1.0与调用入口：https://pypi.org/project/aristotlelib/2.1.0/
  定位：2.1.0 Quick Start / Authentication；关系：method
  支持：证明工具的可调用候选入口。
  限制：未调用；不承诺能完成本例或复现Nexus配置。
  核查：2026-10-20；来源状态：active
- Nexus Erdős125：固定公开证明产物：https://github.com/google-deepmind/alphaproof-nexus-results/blob/0647711a71183c1ea492ad60860776617ce1ea88/APNOutputs/ErdosProblems/erdos_125.variants.positive_lower_density.lean
  定位：同提交仓库README：results collection / not official Google product；关系：direct
  支持：区分研究结果集合与可运行代理。
  限制：可下载证明不等于生成系统可获得。
  核查：2026-10-20；来源状态：active
适用限制：本站未进行该任务的模型运行，不能据此给出本地成功率。

### OpenAI十月公开了内部模型产生的数学研究手稿与部分形式产物，并保留撤回/修订；这直接支持研究产物可逐项审查，不能改写为稳定独立解决大量开放问题。
依据身份：外部报告结果；状态：active
- OpenAI公开新的数学研究产物：https://openai.com/index/sharing-ai-progress-in-mathematics/
  定位：2026-10-06发布；10-15更新内容；对应公开仓库入口；关系：direct
  支持：内部研究模型已公开具体研究产物及验证阶段。
  限制：发布者自报；10-15资助/合作不表示能力新提升；未展示所有公开产品同能力。
  核查：2026-10-19；来源状态：active
- OpenAI十月数学公开产物固定版本与修订：https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a
  定位：README L12-L20/L40-L44；history.md L5-L31；ComparatorChallenges README L12-L28；关系：direct
  支持：固定稿件、模型/人工整理、修订与形式化覆盖可追溯。
  限制：局部形式化和未独立核验需逐稿标注；文本读取不等于全部成果接收。
  核查：2026-10-20；来源状态：active
配置：2026-10-06发布，固定1581d4cb…（10-12）；未发布内部模型；不同成果程序有例外及人工可读性编辑；README算力等值不是实际墙钟/报价，本文不估成功率或完整选题成本。
适用限制：研究产物、正确性、文献新颖性、公开工具可复现四件事分开；撤回/更正须传播到相关主张和引用。
相关进展（本条判断）：
- 公开研究产物让AI数学能力可以逐项检查：/explore?purpose=understand&domain=math&window=all#P-M-RELEASE
  首次公开 2026-10-06；资料修订 2026-10-15：10月15日更新主要涉及资金承诺；数学研究产物的原始公开日仍为10月6日，未据此刷新能力进展。

## 情境变化
### 自然语言研究命题
输入变化：尚无可靠形式化，可能存在含混定义。
判断变化：可整包探索候选论证/反例，同时产出题意核对；不以缺Lean认定不能研究。
验收变化：领域独立审阅关键推导、引用和边界；不能标内核认证。
### 构造/参数优化
输入变化：允许改变算法步长、常数或数学对象，目标约束固定。
判断变化：可联合探索对象和保证；采用建议仍取决于最终证书，不只看最优数值。
验收变化：构造版本、参数精确值与性质证明成对；换对象后保证重新检查。
### 已锁定形式目标
输入变化：只允许修改proof，不允许改变对象或命题。
判断变化：转用W-M01的固定命题证明搜索，毋须重复研究立项。
验收变化：可信声明比对、内核和传递公理强制；不冒充新发现。
### 精确反例
输入变化：目标是反驳全称命题或提出无限反例族。
判断变化：有限命题可直接用精确程序寻找证书；渐近目标需要结构论证。
验收变化：检查全部前提和精确违例；有限计算不能反驳渐近性质。

研究前沿：Nexus研究配置包含进化搜索/AlphaProof并联合探索算法参数与证明；其公开结果可逐项检查。Erdős125是已公开成果复现，不是仍待解决的新问题，也不证明全套系统可调用。 OpenAI十月另公开内部模型研究手稿及部分形式产物，存在不同验证阶段和撤回/修订；这些公开成果属于M04直接证据，不只作为审稿背景。
下一项验证：先在固定Nexus提交重建Erdős125并做题意/传递公理检查，校准复现验收；另选未泄漏问题或允许参数变化的独立小问题，用公开可用工具记录搜索、失败与实际人时。两类结果分开，未运行不估成功率。
未来改判信号：
- 扩大：新问题上，对象/参数与保证共同改进且独立复核成立；题意、文献新颖性和资源记录完备，公开工具可重现。
- 收缩：表面成功依靠弱化目标、无证引理或挑选成功个案；改参数后保证失效；先退到已证引理/候选构造。

## 与本单元直接关联的进展
### 公开研究产物让AI数学能力可以逐项检查
公开 2026-10-06；资料修订 2026-10-15：10月15日更新主要涉及资金承诺；数学研究产物的原始公开日仍为10月6日，未据此刷新能力进展。
OpenAI公开内部前沿模型产生的数学结果，并提供部分Lean形式化和修订机制。
支持范围：公开不等于全部结果已获认可，内部系统能力也不保证当前公开产品可直接复现。
来源状态：active
/explore?purpose=understand&domain=math&window=all&kind=all#P-M-RELEASE

### 证明搜索开始在开放问题上交付可检查结果
公开 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


## 工具与采用佐证