逐題詳解
36,000 題完成第二對話 AI 數理與中英語義覆核;0 題仍為顯示/符號檢查候選。
OCME · 中英數學知識與推導
OCME(開源中文數學百科)持續以中文與英文同步提供知識、教學推導、練習與證據;名稱保留其起點,閱讀入口已是中英雙語。
36,000 題完成第二對話 AI 數理與中英語義覆核;0 題仍為顯示/符號檢查候選。
5 份 Lean 形式證據連結 4 個知識物件;另有 298 個物件尚未登錄形式證據。
查看精確聲明與 Lean 原始碼原題保留 candidate、英文保留 ai_candidate。二次 AI 覆核不是人工審查,也不是全庫 Lean 證明;有限案例只支持明示範圍。
HTML、Markdown 與 JSON 來自相同的公開資料。搜尋、篩選、分頁與中英切換保留網址狀態;題號與既有詳解連結繼續有效。
數學原始資料、公式、AST、來源快照與修訂歷史保留。ISQL-M/SREG 屬內部研究,未在這次網站更新中公開。
AI/純文字閱讀入口 · 公開現況資料 JSON內容生成、雙語檢查、數理覆核、來源採用、形式證明及發布是不同步驟;每份證據只支持其精確聲明。更新不等於提升 Canonical 真值狀態。
CC BY-SA 4.0 · MIT · EveMissLab
可信任來自可見的範圍、可重播的程序、未被刪除的異議,以及人類仍然保有的決定權。
把物件、主張與轉移保存成可驗證事件。
從 Atlas 推導依賴安全的工作批次。
角色輸出遵循明確合約,不直接改 Canonical。
把測試結果綁定到候選 revision。
高風險、同源偏誤與未解異議不被壓平。
以憑證邊界連接外部模型,保存實際模型版本。
保留給跨領域整合與嚴格數學審查。
網站、選題、研究包、MKO、人工觸發批次、發布與跨角色整合。
由前沿模型低頻進行全庫嚴證與架構整合,完成前先討論。
由經核准的高速模型在使用者啟動後,依 brief 生產每批 100 道候選題。