OProver 係一個圍繞 Lean 4 建立的形式化證明框架，重點唔係單次叫模型「寫答案」，而係讓系統一邊嘗試、一邊讀取已驗證證明，再根據編譯器回饋反覆修正。對非研究背景讀者來講，可以理解成 AI 做數學題時，不只交卷一次，而係會睇提示、改錯，再重新整理答案。
實際使用上，這個專案較適合已有 Lean 4 或機器學習環境的人：一類會用它做證明推理與驗證流程，另一類會直接研究訓練管線、資料建構同檢索庫管理。儲存庫同時提供模型與資料方向，包括 OProver-8B、OProver-32B，以及 OProofs 語料，較適合想評估模型表現、重現論文流程，或建立自家證明代理系統的團隊。
它要解決的核心問題，是形式化證明往往唔能夠靠一次生成成功，尤其 Lean 4 對語法、型別同邏輯正確性要求非常嚴格。OProver 的特別之處，在於把「找相似證明」、「接收編譯器錯誤訊息」同「多輪修補」由臨時技巧，變成訓練時已經學會的整體策略，這點比只在推理階段追加外掛模組更完整。
- 支援多輪修正，而唔係只生成一次證明
- 會利用已驗證證明作檢索參考，提升命中率
- 透過 Lean 4 伺服器做機械驗證，結果更可靠
- 提供 CPT、SFT、RL 等訓練流程，覆蓋研究到實作
- 附帶大型 OProofs 資料集，方便分析 pass@k 與修復軌跡
以公開資訊看，OProofs 規模相當大，包含 1.77M 個 Lean 陳述、6.86M 個經編譯器驗證的證明，亦保留失敗嘗試與後續修復過程，這對研究「模型點樣由錯變對」尤其有價值。論文亦提到它在 MiniF2F、ProverBench、PutnamBench 等基準有突出表現；不過這類成果仍主要面向形式化數學、定理證明研究者，同一般應用型開發者的距離會稍遠。
GitHub： https://github.com/multimodal-art-projection/OProver