深度分析 Formal Conjectures：以 Lean4 與 Mathlib 建構的研究級形式化猜想基準 面對自動推理系統快速進展，研究圈提出一套以Lean4形式化的Formal Conjectures基準。它以研究級開放猜想為核心，結合Mathlib與嚴格的Lean核心驗證流程，提供零污染的證明發現測試並同步支援已解題目的自動形式化。該庫已被用於推動新數學發現與建立可重複的評估標準。
