#theorem-prover #dependent-types #lean #parser

nightly oak-lean

Lean theorem prover language parser with support for dependent types and formal verification

4 releases

Uses new Rust 2024

new 0.0.3 Feb 12, 2026
0.0.2 Feb 1, 2026
0.0.1 Jan 23, 2026
0.0.0 Oct 21, 2025

#4 in #dependent-types

MPL-2.0 license

335KB
5.5K SLoC

🚀 oak-lean

Crates.io Documentation

Making LEAN processing simple — A high-performance, incremental LEAN parser built on the Oak framework.

🎯 Project Vision

oak-lean is dedicated to providing industrial-grade parsing support for the LEAN language. By leveraging Rust's high-performance characteristics and Oak's incremental parsing architecture, it can easily handle a variety of application scenarios, from simple script analysis to complex IDE language servers.

✨ Core Features

  • ⚡ Blazing Fast: Fully utilizes Rust's performance advantages to achieve sub-millisecond parsing response times.
  • 🔄 Incremental Parsing: Built-in support for partial updates, demonstrating extremely high efficiency when processing large files.
  • 🌳 Structured Output: Provides a clear, easy-to-traverse syntax tree or data structure.
  • 🛡️ Robustness: Features a comprehensive error recovery mechanism, ensuring normal operation even when input is incomplete.
  • 🧩 Easy Integration: Designed with high cohesion and low coupling, allowing for quick integration into existing Rust projects.

Dependencies

~5–10MB
~105K SLoC