GitHub Repository

OxiLean is a memory-safe, high-performance Interactive Theorem Prover (ITP) natively integrated into the Rust ecosystem. Inspired by Lean 4, it aims to bring formal verification to the Rust community

7 starsRust

OxiLean – Pure Rust Interactive Theorem Prover (Zero C Deps, WASM)

Name: OxiLean – Pure Rust Interactive Theorem Prover (Zero C Deps, WASM)
Availability: InStock
Author: kitasan

by kitasan·Mar 6, 2026·2 points·1 comment

Visit Project View on HN

AI Analysis

●●●BangerWizardryZero to OneBig Brain

Pure-Rust Lean 4 alternative shipping WASM; 99.24% MathLib4 compatibility proven.

Strengths

•Zero-dependency kernel (no unwraps, explicit error handling) is genuinely rare architecture
•Memory-safe design by construction; WASM means browser-first theorem proving
•1.2M LOC with 99.24% MathLib4 compatibility is measurable, not hand-waved

Weaknesses

•Niche audience (theorem provers are narrow); v0.1.0 indicates early-stage despite scale
•Unclear practical advantage over Lean 4 beyond no-C constraint; academic-focused

Post Description

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.