# 推导与反例检查：找出可定位的论证缺口

工作单元：W-M03；版本：2026-10-21.workunits.2；复核：2026-10-20
帮助判断一段推导在给定定义与范围内哪里成立、哪里需要修正。

## 当前用法
适合让AI并行尝试证明、反驳和检索依据；可验证反例可直接推进修订，开放正确性结论仍需更强证明。
依据：Aletheia研究案例展示生成、检查、修订和找反例的作用；公开数学产物允许进一步独立检查。
来源状态：active
本站记录：本站未运行这一单元的AI论证审查试验。

条件：
- 原始论证与定义完整
- 反例可复算，引用可访问
- 接收者能核对领域假设

## 请求与范围
作者已有猜想、证明草稿或数值推导，希望独立找错或找反例。
交付反例、具体缺口或限定检查结论；没找到反例不能当作完整证明。

## 输入
- 论证材料：完整定义、量词、假设、引用和希望检查的结论。
- 检查范围：允许的数值/符号工具、领域范围、可用文献和搜索预算。
- 引用与版本：每个被复用引理的原文、条件及修订状态；论文/证明文件/解释的覆盖对照。

## 交付物
- 逐步假设核对与可定位的问题
- 可复算反例或缺口说明
- 已检范围、无法判断项及下一步证明义务
- 引用命题—本步使用—前提匹配表；可读修订稿区分修复完成与仍未解

## 验收
1. 反例真的满足原前提
   方法：代入原定义独立复算，并解释违反哪条结论
   拒收：反例不在定义域，或改变了原条件。
2. 每步没有偷换条件
   方法：对照量词、极限/交换条件和引用前提
   拒收：把数值抽样通过解释成对全部实数成立。
3. 报告强度匹配检查覆盖
   方法：区分找到缺陷、有限检查未发现、正式证明
   拒收：没找到错误便写“定理已证明”。


## 具体例子
输入：声称对所有实数x都有sqrt(x^2)=x。
预期产物：指出x=-1满足定义域而左侧1右侧-1；应改为abs(x)，或明确增加x≥0。
失败：仅测试x=1、2、3就宣布全称命题成立。

## 工作重组
以前：作者手工推导，同行按顺序读完并寻找疑点。
现在：AI可同时找证明路径与反例，调用符号或数值工具；人按可复算发现修订，关键命题继续形式化。
保留：
- 定义与假设一致
- 研究新颖性和意义判断
新增：
- 区分探索失败和反证
- 核对AI引用确实支持所用步骤

## 人的责任与失败接管
确定问题与结论需要达到的证明强度，判断修订是否改变研究目标；不把同一模型自审当作独立保证。
发现缺口返回位置和所需附加条件；未解决则保留搜索范围，不补造引理或文献。

## 尚待补足
- 用已知正确和带隐蔽缺口的论证校准误报与漏报
- 重要结论可转为W-M01形式化或专项专家审阅

## 职业与团队下一步
研究助理、数学研究、算法论证审查
给出一段原论证、一个有效反例、修订后的条件和仍未解决部分。
对照目标研究方向的理论基础与发表要求；把AI协作过程与本人识别的关键条件分开陈述。
/explore?purpose=career&domain=math
推导尝试太慢，还是专家时间被无效候选占用？
AI扩大候选和反例搜索；工具先淘汰可复算错误，专家集中审阅剩余论证。
按每份有效发现耗费的专家时间比较流程，决定增加搜索预算、形式化基础或专业复核。
/explore?purpose=team&domain=math

## 证据与关系
- Deep Think在专业数学研究中的生成、核查与修订：https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/
  定位：The Frontier of Pure Mathematics；贡献分类；Expanding to Physics and Computer Science；公开 2026-02-11；核查 2026-10-19；复查 2026-10-26
  支持：原作者研究工作流报告。；把搜索和正确性证明分离。
  未覆盖：已投稿不同于已接收；自然语言checker不同内核。；此为任务接收设计，本站未做AI审稿试验。
- OpenAI公开新的数学研究产物：https://openai.com/index/sharing-ai-progress-in-mathematics/
  定位：正文结果发布、Lean材料与修订协议；10月15日资金更新；公开 2026-10-06；核查 2026-10-19；复查 2026-10-26
  支持：支持追踪实际论证与更正影响。
  未覆盖：公开不等于全部有效，也不将新颖性等同正确性。


## 任务级判断与证据
采用方式：探索与候选交付
从证据到建议：外部研究和可修订公开产物说明候选检查有用；可复算反例可独立接收，未发现缺陷只描述搜索覆盖。审查任务不同于完成研究，也不能用同模型赞同自己当独立正确性。
当前可用性：mixed；Aletheia是研究配置；使用公开通用Agent及精确计算/检索可组织候选审查，但不继承内部表现。
- Aletheia研究说明：https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/
  2026-02-11说明；研究方法/产物，不是完整Aletheia自部署包。
- Lean核验（形式交付适用）：https://lean-lang.org/doc/reference/latest/ValidatingProofs/
  按目标项目锁定版本；只用于适用的形式子结论，不强制自然论证走Lean。

### 研究系统已展示把候选生成、检查和修订结合；这提供审查线索，不提供所有自然论证的正确性证书。
依据身份：外部报告结果；状态：active
- Deep Think在专业数学研究中的生成、核查与修订：https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/
  定位：研究案例与方法/限制；Feng26状态；关系：partial
  支持：原作者研究工作流报告。
  限制：已投稿不同于已接收；自然语言checker不同内核。
  核查：2026-10-19；来源状态：active
配置：Aletheia/DeepThink研究系统，专家协作及自然语言检查；任务、干预和预算随个案，不据此估本站概率。
适用限制：已投稿不同于已接收；自然语言checker不同内核。
相关进展（本条判断）：
- 找证明、找反例、返回未解决，成为同一研究循环：/explore?purpose=understand&domain=math&window=all#P-M-ALETHEIA
  首次公开 2026-02-11；判断变化 2026-02-11

### 公开产物和修订入口让论证、引用条件与更正可逐项检查。
依据身份：有条件的编辑推断；状态：active
- OpenAI公开新的数学研究产物：https://openai.com/index/sharing-ai-progress-in-mathematics/
  定位：公开结果及correction/revision入口；关系：method
  支持：支持追踪实际论证与更正影响。
  限制：公开不等于全部有效，也不将新颖性等同正确性。
  核查：2026-10-19；来源状态：active
适用限制：公开不等于全部有效，也不将新颖性等同正确性。
相关进展（本条判断）：
- 公开研究产物让AI数学能力可以逐项检查：/explore?purpose=understand&domain=math&window=all#P-M-RELEASE
  首次公开 2026-10-06；资料修订 2026-10-15：10月15日更新主要涉及资金承诺；数学研究产物的原始公开日仍为10月6日，未据此刷新能力进展。

### 在原前提内可复算的反例或确切缺口可以接收；未找到缺陷必须保留未判定范围。
依据身份：有条件的编辑推断；状态：active
- Deep Think在专业数学研究中的生成、核查与修订：https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/
  定位：研究协作与核查范围；关系：adjacent
  支持：把搜索和正确性证明分离。
  限制：此为任务接收设计，本站未做AI审稿试验。
  核查：2026-10-19；来源状态：active
适用限制：此为任务接收设计，本站未做AI审稿试验。

## 情境变化
### 跨文献引理迁移
输入变化：核心不是算错而是原引理的紧性/可测性/独立性前提。
判断变化：委派引用核对和条件映射，未满足条件则拒绝该步。
验收变化：回到原文核查前提与反例，不能仅比对标题。
### 数值发现
输入变化：反例来自浮点/有限网格。
判断变化：先转精确证书或限定探索范围。
验收变化：精确重算及误差界；未见反例不算证明。

研究前沿：研究系统能交可读数学与部分形式产物，仍有撤回/语义争议；应把可定位的缺口与完整证明分开。
下一项验证：在未泄漏的正确论证与含隐蔽量词/引用缺口论证上校准，保存有效反例、误报和漏报；需要全称保证时转入相应证明任务。
未来改判信号：
- 扩大：新领域论证中能持续给出原前提内的有效缺口，引用核对和独立接收一致。
- 收缩：以浮点异常造假反例、引用不存在，或有限检查被包装成完整证明。

## 与本单元直接关联的进展
### 公开研究产物让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-02-11；判断变化 2026-02-11
DeepMind展示Aletheia等研究协作：生成候选、检查、修订与检索相互连接。
支持范围：作者分级与公开产物支持具体研究贡献线索，不等于全部数学自主完成。本站未逐篇复验，已投稿不同于同行接收，自然语言核查也不同于形式证明内核通过。
来源状态：active
/explore?purpose=understand&domain=math&window=all&kind=all#P-M-ALETHEIA

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


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