Show HN: OxiLean – Pure Rust Interactive Theorem Prover (Zero C Deps, WASM)
Hey HN,
Just dropped v0.1.0 of OxiLean yesterday.
It's a full Interactive Theorem Prover written 100% in Rust (1.2 million lines across 11 crates). Inspired by Lean 4, implements Calculus of Inductive Constructions, universe polymorphism, dependent types, full tactic framework (intro/apply/simp/ring/omega etc.), and even LCNF-based codegen.
Key points that actually matter: - Kernel has literally zero external crates and zero unsafe. Memory-safe by design, no unwraps, explicit errors everywhere. - Runs in the browser via WASM (npm package @cooljapan/oxilean ready). - REPL works out of the box: cargo run --bin oxilean - No C/Fortran anywhere — unlike original Lean.
Repo: https://github.com/cool-japan/oxilean
WASM demo snippet in README if you want to play instantly.
On my machine I've already proven 99.24% of MathLib4's 179,668 declarations (aiming for 100% in 0.1.1 soon). Been grinding this because I got tired of C++/OCaml build hell in formal methods tools.
Curious what you think — especially if you're into formal verification in Rust or using Lean. 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