LeanIn is a concurrency runtime and work-stealing scheduler for Lean 4, inspired by Tokio and Node.js. It demonstrates that high-performance async concurrency patterns can be implemented within a proof assistant using defunctionalisation instead of closures.
Background
Lean 4 is a proof assistant and programming language known for its formal verification capabilities, but it has lacked robust concurrency abstractions comparable to those in mainstream languages like Rust's Tokio.
- Source
- Lobsters
- Published
- Oct 21, 2026 at 07:04 AM
- Score
- 7.0 / 10