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
Thanks for the suggestion. H.264 Baseline/High profile patents are largely expiring between 2027–2028, with a few stragglers potentially lasting until 2030. We're tracking this closely — once the patent landscape is clear, we plan to offer H.264/H.265 as an optional feature. In the meantime, AV1 matches or exceeds H.265 in compression efficiency, so for greenfield projects there's little reason to reach for the legacy codecs.
Fair question. Development was done in a private repo — we squashed the history into a single commit when open-sourcing. That's a deliberate policy choice (clean public history), though I understand it makes it harder to evaluate the project's evolution.
WASM package is already published: https://www.npmjs.com/package/@cooljapan/oximedia — format probing, container demuxing, zero-copy buffers all work in-browser. A live web demo is next on the list.
I built this because I felt standard IPFS is too "static" for the AI era. It's great for storage, but terrible for discovery.
IPFRS attempts to solve this by embedding HNSW Vector Search and a Logic Programming layer directly into the node. This allows you to query the DAG not just by hash (CID), but by meaning (Semantic Search).