Configure and verify Theory2 dependencies.
Configures Lean 4, LeanDojo tracing, and Python environment for Theory2.
/plugin marketplace add slapglif/theory2-physics-plugin/plugin install theory2-physics@theory2-physics-pluginConfigure and verify Theory2 dependencies.
Run the Lean setup script to ensure Lean 4 is properly installed:
bash ${CLAUDE_PLUGIN_ROOT}/scripts/setup-lean.sh
This will:
LeanDojo requires tracing mathlib4 before theorem proving works. This is a one-time operation that takes ~1 hour and requires 32GB+ RAM.
To trace mathlib4:
bash ${CLAUDE_PLUGIN_ROOT}/scripts/trace-mathlib4.sh
Or trace using Python directly:
from lean_dojo import LeanGitRepo, trace
repo = LeanGitRepo("https://github.com/leanprover-community/mathlib4", "v4.3.0-rc2")
trace(repo)
The Theory2 CLI requires a Python virtual environment at /home/mikeb/theory2/.venv.
To verify the Python setup:
/home/mikeb/theory2/.venv/bin/python --version
/home/mikeb/theory2/.venv/bin/theory --help
To run all setup tasks:
# Lean setup
bash ${CLAUDE_PLUGIN_ROOT}/scripts/setup-lean.sh
# Verify Theory2 CLI
/home/mikeb/theory2/.venv/bin/theory --json symbolic compute-e7-alpha
# Check all modules
/home/mikeb/theory2/.venv/bin/theory --json ml info
# Test theorem proving (will trace mathlib4 if not cached)
/home/mikeb/theory2/.venv/bin/theory --json prove lean --statement="2 + 2 = 4" --tactic=norm_num
source ~/.elan/env
lean --version
cd /home/mikeb/theory2
uv sync
/home/mikeb/theory2/.venv/bin/theory --json numerical gpu-status
# Check available memory
free -h
# Tracing requires ~32GB RAM
# If you have less, try with fewer processes:
export NUM_PROCS=4
bash ${CLAUDE_PLUGIN_ROOT}/scripts/trace-mathlib4.sh