radoslawcz/lean4-mathlib

Lean 4.28 + Mathlib4 Environment

Pre-configured Docker image for Lean 4 theorem proving with Mathlib4.

Included

• —Lean 4.28.0
• —Lake (Lean package manager)
• —Mathlib4 project template at /mathlib-template

Usage in HF Jobs

hf jobs run --flavor cpu-basic hf.co/spaces/radoslawcz/lean4-mathlib lean --version

Or with a custom lake project mounted via volume.