[kitasan]

OP here. Just shipped v0.1.1. The big one: Mathlib4 compatibility went from 4,530 to 181,890 declarations tested, hitting 99.7% parse compatibility across the entire Mathlib4 codebase (7,759 files, 280+ categories). This was the #1 thing I wanted to nail before calling OxiLean usable for real math. Most of the work went into a ~6,000-line normalization pipeline that bridges the gap between Lean 4 surface syntax and OxiLean's internal representation. Things like: 280+ Unicode operator replacements (category theory, analysis, algebra, set theory), desugaring multi-binder ∃ into nested Exists(fun ...), normalizing bounded quantifiers, set builder notation, subtype sets, anonymous dot functions ((· < ·) → fun x y → x < y), and a bunch of binder/parenthesization fixes that only show up when you throw 180K real-world declarations at a parser. Test suite also grew from 19 to 769 tests, zero warnings. Still v0.1 territory — the remaining 0.3% failures are mostly exotic notation edge cases — but parsing virtually all of Mathlib4 is the foundation everything else builds on. Elaboration and full type-checking of Mathlib-scale proofs is the next milestone. Repo: https://github.com/cool-japan/oxilean