Add performance benchmarks to README (LeanPython ~6x faster than CPython)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: pirapira

README.md

@@ -78,9 +78,24 @@ LeanPythonTest/    -- Test suite (lexer, parser, interpreter, stdlib)
 
 See `CLAUDE.md` for the full file listing and `PLAN.md` for the development plan.
 
+## Performance
+
+LeanPython is roughly **6x faster** than CPython 3.12 on the leanSpec test suite, despite being a tree-walking interpreter. The compiled Lean4 binary avoids CPython's interpreter overhead and pydantic's heavy metaclass/validation machinery.
+
+| Test | LeanPython | CPython 3.12 | Speedup |
+|---|---|---|---|
+| Constants + exceptions | 0.003s | 0.017s | ~6x |
+| Uint64 arithmetic + codec | 0.009s | 0.092s | ~10x |
+| Container serialize/deserialize | 0.013s | 0.088s | ~7x |
+| Byte arrays | 0.014s | 0.091s | ~6x |
+| SSZVector + SSZList | 0.021s | 0.097s | ~5x |
+| **Total** | **0.060s** | **0.385s** | **~6x** |
+
+Measured on 5 representative leanSpec tiers, each averaged over 3 runs.
+
 ## Design
 
-- **Tree-walking interpreter** -- simpler to implement, debug, and eventually prove properties about. Performance is secondary to correctness.
+- **Tree-walking interpreter** -- simpler to implement, debug, and eventually prove properties about.
 - **Immutable value semantics** where possible, leveraging Lean4's strengths. Python's mutable semantics are modeled explicitly with reference cells on a heap.
 - **Arbitrary-precision integers** via Lean4's native `Nat`/`Int`.