概念導讀
微分法則：以展開求導核對乘積與鏈式規則
以升冪係數列表 f=[2,0,1]、g=[1,3]（即 f(x)=2+x²、g(x)=1+3x）：先由導數定義證明三次以下多項式的求導公式；再以兩條獨立路徑求 (fg)' 與 (f∘g)'——展開後求導，以及使用乘積、鏈式規則——並確認兩者對每個 x 相同；同時核對和與純量倍的規則，指出 f'g'、漏乘內導數、外導數取錯點、反讀係數等錯誤，最後求 x=1 的值。
OCME · 中英數學知識與推導
概念推導導讀
299 份概念教學導讀；另有 36,000 題逐題詳解，兩者分開查找。
概念導讀
原函數：多項式代表原函數、常數族與候選驗收
對 f=[3,−4,6]（f(x)=3−4x+6x²）：由定義證明四次以下多項式的求導公式；構造代表原函數 F0=[0,3,−2,2] 並驗證 F0'=f；證明 F0+C 對每個實數 C 都是原函數，且在至多五個係數的多項式中每個原函數都是 F0+C；驗收候選 G=[7,3,−2,2]（接受）、H=[0,3,−4,2]（拒絕）、K=[0,3,−3,8/3]（兩個測點相符仍拒絕）；求 F0(2)+C（C=−5），並說明原函數不是反函數。
概念導讀
定積分：以左端和的極限與矩公式計算 ∫₀³(x²−4)dx
設 f(x)=x²−4、a=0、b=3。(1) 只用 Riemann 定義（所有合法標記分割和在網格趨 0 時的共同極限）與 f 可積的前提，由 N 等分左端和 L_N 的極限求出 I(f,0,3)；(2) 用本 MKO 明列的矩公式獨立再算一次並核對；(3) 求反向端點的 I(f,3,0)；(4) 以 N=3、N=50 說明有限左端和不等於積分，並說明有號積分不是非負面積。
概念導讀
微積分基本定理：由連續性證明 G′=f，再推出 ∫_a^b f=F(b)−F(a)
設 f:ℝ→ℝ 在全 ℝ 連續，a∈ℝ，G(x)=∫_a^x f(t)dt 為有向積分。(1) 證明 G 在每一點可微且 G′(x)=f(x)；(2) 若 F:ℝ→ℝ 可微且 F′=f，證明對任意實數 a、b 有 ∫_a^b f(t)dt=F(b)−F(a)；(3) 以 f(t)=6t²−2t+1 與候選 F(x)=2x³−x²+x+1/2 算出 ∫_2^{−1} f(t)dt，並說明 G(2)=0 不推出 G′(2)=0、上下限在 x=0 重合也不推出導數為 0。
概念導讀
樹：判定一個 6 頂點圖是樹，求葉、唯一道路與加邊後的唯一環
設 G=(V,E)，V={1,2,3,4,5,6}，E={{1,2},{2,3},{2,4},{4,5},{4,6}}。(1) 依 MKO 定義證明 G 是樹（V 非空、連通、無簡單環）；(2) 列出葉；(3) 求從 3 到 6 的道路並證明它唯一；(4) 加入邊 {3,6}，寫出所形成的簡單環並證明它是唯一的簡單環；(5) 對照：三角形加一個孤立點雖有 |E|=|V|−1 卻不是樹；單點無邊圖是樹但沒有葉。
概念導讀
拓撲空間：完整驗證三點集合上的一個鏈狀開集族，並辨認非拓撲
設 X={a,b,c}（a、b、c 相異）。(1) 證明 τ₁={∅,{a},{a,b},X} 是 X 上的拓撲，涵蓋全部 16 個子族（含空族）；(2) 證明 τ₂={∅,{a},{b},X} 不是拓撲，並指出它通過了哪些檢查；(3) 比較 τ₁ 與不可分拓撲、離散拓撲的粗細；(4) 在 ℕ 上，證明 τ_fin={ℕ 的有限子集}∪{ℕ} 對兩兩聯集與有限交集封閉，卻不是拓撲。
概念導讀
自然數整除：以乘數見證判定、處理 0 的情形並證明遞移性
依 MKO 定義（a∣b ⇔ 存在自然數 k 使 b=a·k）：(1) 證明 6∣84；(2) 證明 6∤87；(3) 證明 4∤10，雖然 10/4=5/2 是一個數；(4) 證明每個 a 都整除 0；(5) 證明 0∣b ⇔ b=0，並說明 0∣0 的見證不唯一、0∤5；(6) 證明 a>0 時見證至多一個（若 a∣b，則既有見證唯一）；(7) 證明整除的自反性與遞移性，並由 3∣6、6∣84 求出 3∣84 的見證。
概念導讀
最大公因數與互質：以整除刻畫驗證歐幾里得算法
依 MKO 的整除刻畫（d∣a、d∣b，且每個公因數 c 都整除 d）：(1) 證明滿足刻畫的 d 至多一個；(2) 證明歐幾里得算法每一步保持公因數集合且必會停止，並以它算出 gcd(84,36)=12，再直接驗證 12 滿足刻畫；(3) 說明公因數 6 不是 gcd；(4) 算出 gcd(8,15)=1，說明 8 與 15 互質但都不是質數；(5) 處理含 0 的情形 gcd(0,1)=1、gcd(0,6)=6、gcd(0,0)=0。
概念導讀
自然數質數：證明 97 是質數、91 是合數，並排除 0 與 1
依 MKO 定義（p 為質數 ⇔ 2≤p 且 p 的每個自然數因數 d 都滿足 d=1 或 d=p）：(1) 說明 0 與 1 不是質數；(2) 證明 2 是質數；(3) 以見證 7 證明 91 是合數，並說明只測 2、3、5 會誤判；(4) 證明「若 n=dk 且 d、k≥2，則 min(d,k)²≤n」，據此只需檢查 2 到 9，證明 97 是質數；(5) 證明 2 是唯一的偶質數。
概念導讀
自然數模同餘：餘數定義、見證形式、運算保持與取消的限制
依 MKO 定義（n>0，a≡b (mod n) ⇔ a mod n=b mod n）：(1) 判定 100≡23 (mod 7)；(2) 證明它等價於見證形式「存在自然數 k、l 使 a+nk=b+nl」，並給出 100 與 23 的見證；(3) 說明同餘是等價關係；(4) 證明加法與乘法保持同餘，並由 15≡1 (mod 7) 得 115≡24、1500≡23 (mod 7)；(5) 以 2·3≡2·0 (mod 6) 說明不能無條件取消公因子；(6) 說明不同模數不能串接，並說明模數 0 被排除。
概念導讀
決定問題：在明示有限輸入集上證明試除程序是 decider
取輸入集合 X={0,1,2,3,4,5,6,7,8,9}、規格 P(x)：「x 是質數」與 yes-instance 集合 Y={x∈X ∣ P(x)}。在明示的 while 程式計算模型 W 中，證明試除程序 D1 對每個 x∈X 都終止，且 D1(x)=true 當且僅當 x∈Y，因此 D1 是 (X,Y) 的 decider；再說明只在 yes-instance 上停止的 D2 與只看奇偶的 D3 都不是 decider。
概念導讀
證明助理中的形式陳述：逐層讀懂一個 Lean 陳述並區分「是陳述」與「已證明」
以源碼字串 s：`∀ (a b : Nat), a ≤ b → a < b + 1` 為教學對象，在一個明示固定但未實際執行的環境 E 中逐層說明：它的約束變數與型別、假設與結論、若 elaboration 成功應得到的核心項 S、為何 S 的型別會是 Prop、一個證明項必須建立什麼；再給出其數學內容的非正式證明，並以 s′：`∀ (a : Nat), a - 1 < a`（是 Prop 但為假）與 s″：`∀ (a : Int), a - 1 < a`（為真）對照。全程未執行 Lean，不宣稱任何內容可解析、可 elaboration、已編譯或已被 Lean 證明。
概念導讀
開集與閉集：在四點拓撲中完整分類十六個子集
設 X={1,2,3,4}，τ={∅,{1},{1,2},{3,4},{1,3,4},X}。先驗證 τ 是 X 上的拓撲，再列出全部閉集，並把 X 的十六個子集分成「既開又閉」「只開」「只閉」「既不開也不閉」四類；最後證明在任何拓撲空間中 ∅ 與 X 都既開又閉，以及兩個閉集的聯集仍是閉集。
概念導讀
鄰域：在四點拓撲中搜尋開集見證並列出全部鄰域
設 X={1,2,3,4}，τ={∅,{1},{1,2},{3,4},{1,3,4},X}。判定 N1={1,2,3} 與 N2={2,3,4} 是否為點 2 的鄰域；證明在有限拓撲中，點 x 的鄰域恰是包含 O_x（含 x 的全部開集之交）的子集，據此列出點 1、2、3、4 的全部鄰域；證明鄰域向上封閉；並說明同一集合在離散拓撲下的判定可能不同。
概念導讀
拓撲連續映射：在有限空間中用逆像判定連續，並與開映射區分
設 X={1,2,3}，τX={∅,{1},{1,2},X}；Y={a,b}，τY={∅,{a},Y}。對三個以完整表格給出的映射 f（1↦a、2↦a、3↦b）、g（1↦a、2↦b、3↦a）、c（全部 ↦b），用逆像條件判定是否連續，並判定是否為開映射；證明連續映射的合成仍連續並以 q:Y→Z 驗證；最後數出 X→Y 的全部連續映射。
概念導讀
抽象計算模型：在七狀態模型中截斷停止邊、計算可達集並區分停止、卡住與不終止
給定有限模型 (S,Init,Step,Halt)：S={s0,s1,s2,s3,s4,s5,s6}，Init={s0}，Halt={s3}，原始邊資料 {(s0,s1),(s0,s2),(s1,s3),(s1,s5),(s2,s4),(s4,s2),(s3,s6)}。依 MKO 規則截斷停止狀態的外出邊，以不動點迭代算出可達集，找出停止狀態、卡住狀態與可達循環，給出合法的停止、卡住與無窮執行，排除三條不合法的 trace，並說明為何尚未窮盡可達圖的有限深度探索，不能僅憑未見反例就斷言所有極大執行終止。
概念導讀
算法正確性：非確定性相鄰交換排序的部分正確、終止與總正確
在有限狀態模型 M 中，狀態是 (1,2,3) 的六個排列，初始狀態 (3,2,1)，每步可非確定性地交換任一個相鄰逆序對，Halt={(1,2,3)}。以後置條件「遞增排列且為輸入的重排」證明 M 的部分正確性、終止性與總正確性：用排名函數 inv（逆序數）證明每條執行至多 3 步，且每條極大執行停在 Halt。再以變體 M′（允許交換任何相鄰對）說明一條成功路徑與部分正確都不足以得到總正確，以變體 M″（錯誤的停止條件）說明終止不足以得到正確。
概念導讀
漸近資源界：證明 3n²+5n+2∈Θ(n²) 並排除 Θ(n)
設成本函數 f(n)=3n²+5n+2（n 從 0 起），比較函數 g(n)=n² 與 h(n)=n。以明示的全尾段 witness 證明 f∈O(g)（c=10、N=1）、f∈Ω(g)（c=3、N=0），故 f∈Θ(g)；說明 N=0 對 O 不可行、c=3 對 O 不可行、另一組 witness c=4、N=6 也可行；再證明 f∉O(h)，因此 f∈Ω(h) 但 f∉Θ(h)。
概念導讀
證明項：逐部分解讀 λh. ⟨snd h, fst h⟩ 為何是 P∧Q→Q∧P 的證明項
在一個明示的合成小型命題型別系統 ST 中（對應 MKO 假設 a2），取相異命題原子 P、Q：逐部分說明項 t=λh:P∧Q. ⟨snd h, fst h⟩ 的每一部分建立了什麼、具有什麼型別，推導判斷 ⊢ t : P∧Q→Q∧P，並說明 t 的型別為什麼與命題 S=P∧Q→Q∧P 相符；再證明外觀相近的 t′=λh:P∧Q. ⟨fst h, snd h⟩ 不是 S 的證明項。最後區分「ST 中的型別推導」「Lean kernel 接受」與「已保存的 proof-term receipt」三者。
概念導讀
離散時間動力系統：在七個狀態上迭代 T(x)=(3x+1) mod 7
狀態空間 X={0,1,2,3,4,5,6}，更新映射 T(x)=(3x+1) mod 7。由 x_0=0 依 x_(n+1)=T(x_n) 算出軌道，證明對所有自然數 n 有 x_(n+6)=x_n，據此求 x_2026；完整枚舉固定點；判定 A={0,1,2,4,5,6} 是正向不變子集而 B={0,1} 不是，並證明從 0 出發的軌道永遠不會到達固定點。
概念導讀
常微分方程：判定階數並核對候選解 y=x² 與 y=x²+x
在區間 I=ℝ 上考慮常微分方程 y″−2y′+y=x²−4x+2。(1) 判定它的階數；(2) 核對 y₁(x)=x² 在整個 ℝ 上是解（殘差恆為零）；(3) 證明 y₂(x)=x²+x 的殘差是 x−2，只在 x=2 為零，所以它不是 ℝ 上的解；(4) 核對初值 y(0)=0、y′(0)=0，並引用二階線性方程的存在唯一定理（含其假設）判定 y₁ 是此初值問題的唯一解；(5) 說明沒有初值時解不唯一。
概念導讀
數值近似與誤差：以 0.33 近似 1/3 的絕對誤差、相對誤差與容許範圍
以精確有理數計算：近似值 a=33/100 相對參照值 x=1/3 的絕對誤差與相對誤差；判定 a 是否在容許誤差 τ₁=1/250、τ₂=1/400、τ₃=1/300 之內（τ₃ 為端點情形）；證明 |a−x|≤τ ⇔ x−τ≤a≤x+τ；比較放大 1000 倍後的誤差；說明參照值為 0 時相對誤差沒有定義，以及誤差數值本身不能說明誤差來源。
概念導讀
最佳化問題：在九個整數候選中先判可行、再比較目標值
候選集合 C={0,1,2}² 共九點，限制 x+2y≥3，目標函數 f(x,y)=x+y。以「先判定可行性、再逐一比較」的掃描演算法求最小值，並以不變量證明結果：最優值 m=2，argmin={(0,2),(1,1)}（兩個平手）；說明 (0,0) 與 (2,0) 雖然目標值不大於 2 卻不能入選；求最大值；並說明同一限制在實數非負象限上的最小值為 3/2，其達到點 (0,3/2) 不在宣告的有限候選集合中。
概念導讀
量綱分析：以指數向量核對 ½mv²=mgh 並排除 v=2gh
以基本量綱 L、M、T 的整數指數向量 d(Q)=(a,b,c)：算出速度、加速度與兩種能量式的量綱；判定 ½mv²=mgh 量綱一致、v=2gh 不一致且無法以純數常數修正、v²=4gh 量綱一致卻在等加速度模型中錯誤；判定 m+v 不能相加；由 E=C·m^α v^β 解出 α=1、β=2；並說明量綱相同不代表單位換算因子相同。