WHY TRIZ?
我们刻意选择了一个极其冷门的工程方法论来验证 AI 的工程能力。
TRIZ 基于 20 万件高水平专利的提炼，包含 40 个发明原则、39 参数矛盾矩阵、76 个标准解——这些复杂的工程知识体系，AI 都能理解并运用。
连 TRIZ 这么冷门的方法论都能驾驭，你的制造业问题只会更简单。
TRIZ SKILL 已适配以下 Agent 平台
40 INVENTIVE PRINCIPLES
SOLVE · 矛盾速解
教学演示到此为止——真刀真枪的速解,在专门的工具页:用自己的话描述矛盾, 落到 39×39 全量矩阵,查到的每条原理直接接「生成候选解 / 交证书 / 记结果」。
TRIZ TOOLS
TRIZ IN ACTION
外面很冷，你戴了厚厚的保暖手套。这时手机响了，你想接电话或回微信。
如果不摘手套 → 屏幕没反应（普通手套不导电）
如果摘手套 → 手指冻得疼，还可能冻伤
典型的技术矛盾
想要保暖（戴厚手套），同时想要操控触摸屏（需要导电）——一个变好，另一个就变坏。
很多人是偶然发现或模仿别人，不知道原理
忍受寒冷露出一个手指来操作
在手套指尖剪个洞——既不保暖又难看
这些方法要么靠试错、要么靠运气，不知道下一次遇到类似问题该怎么系统化思考。
参数：手套的导电性。想导电触屏又不想导电保暖，同一个参数需要两种相反状态。
用时间分离：同一个位置在不同时间需要不同状态。操作屏幕时导电，其他时候保暖。
导电纤维手套：指尖用导电材料，其余部分保暖。矛盾被局部化解决，不需要妥协。
小到手套、杯子，大到发动机、芯片散热，本质都是一样的——消除矛盾。不一定要学完所有工具，先从物理矛盾+分离原理入手就能解决很多问题，避免瞎试、拍脑袋，用一套有逻辑的方法快速定位矛盾核心。
AI × LEAN 4 · NEW CHAPTER
上面是 TRIZ 的完整工具箱。这一章是我们的新篇:用 AI 时代的新方法把火花激活——问题 = 定理,答案 = 证明, LLM 搜索生成,Lean 内核裁决;发明原理成为可检索的策略条目,应用结果滚动校准原理库。 「找答案」由此拆成两个难度差一个量级的问题:判定是搜索问题(交给 AI 发散),验证是类型检查问题(交给内核收口)。
状态:探索路线图(v0.1,未实施)。排期与 Kill Criteria 公开见下文,先立后跑。
THREE PILLARS
TRIZ 的发明原理是策略库的核心资产。入库时每条补上显式前提谓词 + 方向性效果声称 + 历史应用成败记录,以策略条目身份进入 AI 检索层——火花负责点燃,证据负责落地。
AI 提交的每个「解」必须附带构造性证书;Lean 4 只当证书检查器——验链条、不找答案。判定「缺什么」是搜索问题,验证「补全是否成立」是类型检查问题,难度差一个量级。
策略库按真实应用结果滚动校准:track-record × 近期加权,推荐分随证据更新。未校准的条目照常展示前提、不展示推荐分——未校准不装作有把握,火花越用越准。
HARD CONTRACTS
验证者高于生成者 · 原理不作公理 · 每次应用记结果——三条是硬契约,不是愿景。 违反任何一条,这套思路就退化成「又一个说得像对的方法论」。
Lean 内核是裁决者。AI 生成的一切候选,不过内核就不算数;生成器再强也无权盖章。
发明原理值得检索、值得尝试,但结论由证书说话。火花不需要为「绝对正确」背书,只需要在应用中被记录、被校准——这反而让火花被保护。
应用一次记一行台账,公开结清。策略条目的推荐分从记录里长出来,而不是从声称里长出来。
PHASE 1 · CERTIFICATES
物场分析是 TRIZ 的经典建模。这一步做的不是替换,是转译—— 让物场与缺陷谓词在 Lean 里获得可检查的形式,火花因此能被机器把关。 物场模型 = 三元组 (S1, F, S2): 物质 1 经场 F 作用于物质 2。完整物场才具备「可工作」资格;问题情境 = 物场 + 缺陷谓词。
关键设计决策:Lean 不判定「缺什么」,只验「提交的补全是否成立」。AI/人 提交的不是结论,是构造性证据——补全元素 + 补全后的完整物场 + 两个小步证明; 小步谓词走 Decidable 机械检查,推导里的 sorry 必须显式声明(置信记「可能」,不冒充已证)。
「钉子要尖利(穿入)vs 易运输(不伤人)」—— 抽象:S1=钉身,F=机械场,S2=目标物;缺陷 = 有害作用「尖锐端暴露」。 提交证书:引入第三种物质 S3 包装物(隔离场)→ 物场完备 → 缺陷谓词被消解 → 内核通过。
验收不是「能跑通」,是同一套 SuField/Defect/Certificate 定义 原封不动再解一个非钉子案例(备选:快递柜 vs 防盗)。两个案例共用全部定义才算过—— 这是 adequacy check 的机械替代,防玩具形式化。
RETRIEVAL LAYER
策略库的条目,就是 TRIZ 的发明原理——入库时带上三样东西: 显式前提谓词 + 方向性效果声称 + 历史应用成败记录。 检索 = 前提可满足性检查:前提不满足的条目直接拒——拒绝发生在检索层,不在逻辑层; 条目作火花、不作公理,进不了 Lean 的 trusted 层。 活演示见 /solve 矛盾速解(策略条目卡 + 校准台账,未校准不给推荐分)。
PHASE 2 · CALIBRATION
每行台账记下应用当时的 weight_snapshot——校准过程本身可审计,事后能复现「当时为什么推荐它」。 汇报指标:每条目的应用次数、成功率、加权成功率与校准分(预测「有效」的准确率 vs 实际),配校准曲线。
主张句:「第一个可校准的发明原理库」——Lean 侧提供证明的严谨,TRIZ 侧攒了半世纪的发明火花,再接上实证校准: 把两边接起来的交叉点,就是我们。
ROADMAP & KILL CRITERIA
| 周 | 事项 | 出口 |
|---|---|---|
| W1–2 | Lean 4 基础 + Su-Field/Defect/Certificate 骨架 | 骨架编译通过,sorry 显式标注 |
| W3–4 | 钉子案例 + 第二个案例端到端 | 双案例共用定义验收 |
| W5–6 | 策略条目检索原型(前提全部显式化) | 检索结果人工盲评 ≥ 翻书基线 |
| W7–8 | 校准闭环 MVP:手工喂案例跑通记账 | weight_snapshot 链路通 |
| 持续 | 闭环接语料 + 接 AI 生成器 | — |
先立后跑 · KILL CRITERIA
双案例验收中若第二个案例需要改动 Defect 定义,说明抽象是给单个案例特设的——停,或回炉重设抽象。
策略条目检索的人工盲评若不优于翻书基线,证明「前提显式化」本身无实用价值——项目降级为纯研究,停止工程投入。
20 案例校准后若所有条目权重无区分度(全接近 0 或全接近 1),说明闭环无矿可挖——转人工策展模式。
BOUNDARIES
FAQ
发明原理是火花,也是策略库的核心资产:我们继承它、显式化它的前提、用证书把关它的每次应用、用真实结果滚动校准它——这就是「AI 时代用新方法激活 TRIZ 的火花」。AI 时代的工具不为取代火花,为让火花可检索、可检验、可成长。
这是思路与路线图(探索稿 v0.1,先立后跑)。Kill Criteria 公开立在前面,到点对账;在通过验收之前,本篇不声称任何已交付的引擎或产品。
内核小到可以信任:每一步推导都经类型检查;构造性证明即程序,能从证明里提取可执行解法;LLM×Lean 的搜索-验证生态是当前最活跃的形式化 AI 前线之一。
会,而且经常错。所以正确性从来不押在生成侧——AI 说的不算数,内核通过的才算数。生成器可以随便发散,垃圾进不了 trusted 层。
分工是:人提出问题、定验收判据、做形式化;AI 生成候选证明与引理分解;内核裁决每一步。不需要人人都会写 tactic,但「什么算解决」必须由人说清。
提示词工程优化「说得像对」;这套思路要求「交出可检查的证据」。前者对输出措辞下功夫,后者对输出的正确性给出机械的通过/不通过。
不值得。形式化有成本,判据模糊、错了也无所谓的问题用轻量方法就好。判据清晰、错不起验证的问题,才配得上让内核把关。
DEEP DIVE
Lean 骨架、策略条目结构、台账 schema 与 LLM×Lean 生态——不看这一段,不影响使用主线的思路。默认收起。
描述你的技术矛盾，TRIZ 将为你推荐最适合的发明原则与解决方案
SKILL 载体 · TRIZ 生成候选 → SVV 机器裁决 → 应用记结果