模型發布
小紅書模型據報IMO滿分
量子位據報導
據量子位報導，小紅書大模型 dots-note-3.0 在 IMO 2026 官方評測中答對全部六題，以 42 分獲得金牌。模型直接閱讀英文題目並以自然語言完成證明，推理過程結合 Python 程式執行與遞迴式自我批判。報導稱該模型將開源，但尚未提供時間與授權等細節。
讀原始報導背景
新聞提到的 Lean 是以依賴型別理論為基礎的互動式定理證明器，也是一門程式語言，由微軟研究院於 2013 年啟動開發。它能將數學定理轉換為嚴格的形式化表達，並透過電腦驗證證明的正確性。