Warning: This codebase was vibe-coded in a few hours with Claude. Do not use this for anything of value.
No theorem proving is involved yet. This is plain Lean4 code that happens to be written in a language with a proof assistant — we're not using that capability at this stage.
LeanPython is a tree-walking Python 3.12 interpreter written in Lean4. The end goal is to interpret the leanSpec Ethereum consensus specification, making Python specs usable from within Lean4. Right now it can run basic Python programs with arithmetic, control flow, functions, lists, dicts, comprehensions, and a handful of built-in functions.
Install elan (the Lean version manager):
curl https://elan.lean-lang.org/elan-init.sh -sSf | shClone and build:
git clone https://github.com/zksecurity/leanPython.git
cd leanPython
lake buildThe first build downloads the Lean toolchain and compiles everything — this takes a few minutes.
Write a Python file and run it:
echo 'print("Hello, World!")' > hello.py
lake exe leanPython hello.pyRun the test suite:
lake testThe codebase is still rapidly changing and the author is pushing to main directly. Please wait for things to stabilize before opening PRs.