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.