# 數學證明

數學證明是在明示的前提與推理規則下，建立指定結論的可檢查論證。

mko-proof · concept · v0.10.0



## 數學敘述

給定待證命題 P，證明必須在指定語境中由已接受的前提、定義、公理或先前結果，經合法推理得到 P。





## 代表公式（精確 TeX）

P





## 成立條件


- 已明示待證命題、可使用的前提與推理語境。





## 符號作用域


- P — 待證命題





## 直觀、定義與常見誤解

證明的任務不是只累積支持例子，而是說明結論為何由明示條件必然成立。單一有效反例可以否定全稱命題；有限正例若沒有證明論域有限、枚舉完整且每個案例成立，便不能單獨建立一般命題。

直接證明從前提向結論推進；反證法則加入結論的否定並導出矛盾。採用哪種方法仍須尊重所處邏輯系統可用的規則。

形式證明把陳述與每個推理步驟交給形式系統檢查；非形式證明也必須讓讀者能追蹤前提、推理與結論。

常見誤解是把數值抽樣、圖形外觀、權威引用或未交代規則的直覺當成一般證明。





## 已採用的推導導讀

[數學證明：證明 n²+n 恆為偶數，並以反例否定「n²+n+41 恆為質數」](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-proof-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [邏輯連接詞](https://ocme.evemisslab.com/zh-Hant/mko/mko-logical-connectives/) — 證明必須能辨識待證命題及其邏輯結構。





## 驗證界線

有限測試或例子若缺少有限論域與完整枚舉的證明，只能支援指定實例；即使完成窮舉，也必須檢查完備性論證與定理聲明。自動搜尋若產生一般證明，則必須另行檢查定理聲明、前提、推理規則與證明物件。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

選定具體定理陳述，綁定其前提、結論、Lean proof term 與可重現檢查 receipt。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/proof.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-proof/index.md)