OUKC Lean 4 進捗
概要 / Description
日: OUKC Lean 4 corpus 進捗. 2,188 theorems / 78 closed-by-rei zero-sorry / Brocard n=[1,150] (165 theorems) / Mathlib auxiliary 拡張中.
EN: OUKC Lean 4 corpus progress. 2,188 theorems / 78 closed-by-rei zero-sorry / Brocard n=[1,150] (165 theorems) / Mathlib auxiliary library expanding.
OUKC は friendly parallel as Mathlib として独立に Lean 4 formalization を継続.
現状 (2026-05-02): 2,188 Lean 4 theorems / 78 closed-by-rei zero-sorry / Brocard n=[1,150] full closure (165 theorems).
Mathlib にはAI policy 尊重で AI 生成 PR を投稿せず、OUKC commons 内で independent 蓄積.
詳細は SPA 内 Lean Progress page で realtime 表示.