Fair points. "Production-ready" was probably too strong for v0.1.0 — "API-stable" is more accurate. The crates compile, pass their test suites, and the public API surface is locked, but real production readiness comes from users hitting edge cases we haven't. (no warnings policy etc.) On line count — you're right that more lines isn't inherently better. I mentioned it as a scale indicator, not a quality claim. The meaningful numbers are the 92 crates, the codec/container/protocol coverage, and the test results. Happy to discuss any specific module if you want to dig into the details.

Understood. Development was in a private repo, squashed on open-source. I know that makes evaluation harder — we'll publish incremental commits going forward.

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