Date: 2026-01-01
Status: Architecture Decision Record
Impact: 🔴 Major - 改變整個系統核心設計
概念：為每類問題預先定義完整的推導步驟模板
# 範例：安全帶張力分析模板
template:
id: seatbelt_tension_analysis
parameters: [M1, M2, v, m, k]
steps:
- id: 1
formula: "M1 * v = (M1 + M2) * v_f"
solve_for: v_f
- id: 2
formula: "Delta_v = v - v_f"
- id: 3
formula: "(1/2) * m * Delta_v**2 = (1/2) * k * x**2"
solve_for: x
- id: 4
formula: "T_max = k * x"問題：
- ❌ 無法窮舉所有可能的問題
- ❌ 每個新問題都需要新模板
- ❌ 無法處理問題變體（例如：加入摩擦力）
- ❌ 缺乏理論基礎追溯
User: "公式可能是被證明的（但也是理想化的）... 但公式可以變化：例如 F=ma，但加入摩擦力呢？"
核心問題：
- 公式來自理想化定理（Lean4 可證明）
- 現實問題需要修正項（friction, drag, heat_loss...）
- 不可能為所有「理想化 + 修正組合」預先建模板
類比：
- ❌ 錯誤：為每道菜預先寫好完整食譜
- ✅ 正確：提供基礎烹飪技法 + 食材庫，可組合創造
核心概念：Principle + Modifications → Derived Form
┌──────────────────────────────────────────────────────────┐
│ 基礎原理 (Principles) │
│ - Newton's 2nd Law: F = ma [Lean4 證明 ✓] │
│ - Momentum Conservation [Lean4 證明 ✓] │
│ - Energy Conservation [Lean4 證明 ✓] │
└──────────────────────────────────────────────────────────┘
↓ + 修正項
┌──────────────────────────────────────────────────────────┐
│ 修正項庫 (Modifications) │
│ - Friction: -μ * N │
│ - Air Drag: -(1/2) * ρ * v² * Cd * A │
│ - Heat Loss: -h * A * ΔT │
└──────────────────────────────────────────────────────────┘
↓ 動態組合
┌──────────────────────────────────────────────────────────┐
│ 推導引擎 (Derivation Engine) │
│ - 根據問題特徵選擇 principle │
│ - 根據現實條件添加 modifications │
│ - 編譯成 sympy-mcp 調用序列 │
│ - 驗證維度和合理性 │
└──────────────────────────────────────────────────────────┘
↓ 結果
┌──────────────────────────────────────────────────────────┐
│ 精確計算 + 推導追溯 + (可選) Lean4 證明 │
└──────────────────────────────────────────────────────────┘
格式：
# formulas/principles/newtons_second_law.yaml
principle:
id: newtons_second_law
name: 牛頓第二定律
# 基礎形式（理想化）
base_form: "F = m * a"
# Lean4 驗證
lean4_reference:
module: "Mathlib.Physics.Classical.Newton"
theorem: "newton_second_law"
proven: true
# 變數定義
variables:
F: {description: "合力", unit: "N", type: "vector"}
m: {description: "質量", unit: "kg", type: "positive_real"}
a: {description: "加速度", unit: "m/s²", type: "vector"}
# 適用條件
conditions:
- "質點近似或剛體"
- "慣性參考系"格式：
# formulas/modifications/friction.yaml
modification:
id: friction
name: 摩擦力
# 數學表達
term: "- mu * N"
# 物理意義
description: |
摩擦力與正向力成正比，方向與運動方向相反
# 適用條件
conditions:
- "有接觸面"
- "有相對運動或運動趨勢"
# 變數
variables:
mu: {description: "摩擦係數", type: "positive_real", typical_range: [0, 1]}
N: {description: "正向力", unit: "N", type: "positive_real"}
# 典型數值
typical_values:
static_friction:
steel_on_steel: 0.74
rubber_on_concrete: 0.9
ice_on_ice: 0.1
kinetic_friction:
steel_on_steel: 0.57
rubber_on_concrete: 0.7
ice_on_ice: 0.03@mcp.tool()
def derive_variant(
principle_id: str,
modifications: list[str],
solve_for: str = None
):
"""
推導變體公式
Example:
derive_variant(
principle_id="newtons_second_law",
modifications=["friction", "air_resistance"],
solve_for="a"
)
返回：
{
"derivation_steps": [
{"step": 0, "equation": "F = m * a", "description": "基礎形式"},
{"step": 1, "add": "friction", "equation": "F - μN = m * a"},
{"step": 2, "add": "air_resistance", "equation": "F - μN - (1/2)ρv²CdA = m * a"},
{"step": 3, "solve": "a", "result": "a = (F - μN - (1/2)ρv²CdA) / m"}
],
"final_form": "a = (F - μN - (1/2)ρv²CdA) / m",
"lean4_traceable": true
}
"""社群貢獻的常見問題預組合：
# formulas/derived_forms/mechanics/sliding_with_friction.yaml
derived_form:
id: sliding_with_friction
name: 斜面滑動（含摩擦）
based_on:
principle: newtons_second_law
modifications: [gravity, friction]
derivation:
- base: "F = m * a"
- add_gravity: "m * g * sin(θ) + ... = m * a"
- add_friction: "m * g * sin(θ) - μ * m * g * cos(θ) = m * a"
- simplify: "a = g * (sin(θ) - μ * cos(θ))"
final_form: "a = g * (sin(theta) - mu * cos(theta))"
# 仍然可追溯到基礎原理
traceable_to: "newtons_second_law"❌ 舊系統（黑箱）
User: "車 1500kg，50km/h，濕路面 μ=0.3，剎車距離？"
System: "公式是 s = v²/(2μg) = 32.8m"
User: "為什麼？"
System: "..." (無法解釋)
✅ 新系統（可追溯）
User: "車 1500kg，50km/h，濕路面 μ=0.3，剎車距離？"
Agent: "讓我從基礎推導：
Step 1: 基礎原理
牛頓第二定律: F = ma
來源: Mathlib.Physics.Classical.Newton [Lean4 證明 ✓]
Step 2: 識別受力
問題提到「剎車」「濕路面」
→ 需要添加 friction modification
Step 3: 應用修正
F = ma
剎車力來自摩擦: F = -μmg
代入: -μmg = ma
簡化: a = -μg
Step 4: 運動學計算
v² = v₀² + 2as
剎車到停止(v=0): 0 = v₀² + 2(-μg)s
解出: s = v₀²/(2μg)
Step 5: 代入數值
v₀ = 50 km/h = 13.89 m/s
s = (13.89)²/(2 × 0.3 × 9.8) = 32.8 m
結論: 剎車距離 32.8 公尺"
User: "完全理解了！"
┌─────────────────────────────────────────────────────────┐
│ Lean4 + Mathlib (形式化證明) │
│ - 提供基礎定理的數學證明 │
│ - 保證 principles 的邏輯正確性 │
│ - 類型檢查、定理證明 │
└─────────────────────────────────────────────────────────┘
↓ 理論基礎
┌─────────────────────────────────────────────────────────┐
│ NSForge (推導編排) │
│ - 橋接形式化定理和工程應用 │
│ - 提供 principles + modifications │
│ - 動態組合推導 │
│ - 維度檢查、合理性驗證 │
└─────────────────────────────────────────────────────────┘
↓ 推導步驟
┌─────────────────────────────────────────────────────────┐
│ sympy-mcp (符號運算) │
│ - 精確執行每一步計算 │
│ - 解方程、積分、微分 │
│ - 符號簡化、代數操作 │
└─────────────────────────────────────────────────────────┘
關鍵差異：
| 系統 | 做什麼 | 不做什麼 |
|---|---|---|
| Lean4 | 證明定理的邏輯正確性 | 不做數值計算、不處理實際問題 |
| NSForge | 提供推導框架、組合公式 | 不做符號運算、不做形式化證明 |
| sympy-mcp | 執行精確符號運算 | 不知道該用什麼公式、不驗證物理意義 |
- 設計 principles 格式
- 設計 modifications 格式
- 實作
derive_variant()MCP tool - 建立第一組範例：Newton's 2nd Law + friction
- Audio Circuits: 音響電路學
- Op-amp 濾波器設計
- 頻率響應分析
- 失真分析
- 阻抗匹配
- Pharmacokinetics: 藥物動力學
- 一室/二室/三室模型
- 首過效應
- 藥物清除率
- 穩態濃度
- Mechanics: friction, drag, springs, gravity（基礎）
- General Circuits: resistance, capacitance, inductance
- Thermodynamics: heat_loss, non_ideal_gas
- 標註每個 principle 的 Lean4 來源
- 實作
verify_with_lean4()tool - 建立 Lean4 ↔ NSForge 映射
- 提供 modification 貢獻模板
- 建立 derived_forms 審核機制
- 文檔和教學範例
-
用戶洞察（2026-01-01）
"公式可能是被證明的（但也是理想化的）... 但公式可以變化：例如 F=ma，但加入摩擦力呢？"
關鍵認知：不可能窮舉所有問題，應該提供可組合的基礎單元
-
Stephen Diehl - sympy-mcp 專案
- 論文："The Future of Math is Weird"
- GitHub: https://github.com/sdiehl/sympy-mcp
- 啟發：LLM 不擅長符號運算，應該用專門工具（sympy）
-
Lean4 + Mathlib
- 形式化數學證明系統
- 提供理論基礎來源
- 保證公式的數學正確性
- Domain-Specific Languages (DSL)：半形式化表達層
- Component-Based Design：可組合的設計模式
- Microkernel Architecture：核心小、可擴展
| 模組 | 影響 | 遷移策略 |
|---|---|---|
templates/*.yaml |
🔴 格式改變 | 轉換為 derived_forms |
tools/template.py |
🔴 大幅重寫 | 改為 derivation.py |
docs/template-system-design.md |
🟡 需更新 | 標註為舊版 |
| MCP Server 接口 | 🟢 新增工具 | 向後兼容 |
優點：
- ✅ 可以處理更多問題變體
- ✅ 推導過程清晰可追溯
- ✅ 教育價值提升
- ✅ 理論基礎明確（Lean4）
潛在挑戰：
⚠️ Agent 需要更多推理（選擇 modifications）⚠️ 初期 principles 數量有限⚠️ 需要建立良好的錯誤提示
決策：採用「可組合推導框架」取代「完整模板系統」
批准：Architecture Decision (2026-01-01)
下一步：實作第一組 principle (Newton's 2nd Law) + modification (friction)
- 原始設計：docs/template-system-design.md
- 架構文檔：memory-bank/architect.md
- 決策日誌：memory-bank/decisionLog.md
- sympy-mcp 發現：memory-bank/research/sympy-mcp-discovery.md
Revision History:
- 2026-01-01: 初始版本 - 記錄從模板到框架的演化