Remove Lean+Mathlib warmup step from Dockerfile

The warmup triggered a full Mathlib download which exceeded HF Spaces
build limits. Mathlib will now be cached lazily on the first user request
instead of at build time.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Dockerfile

@@ -24,12 +24,6 @@ RUN pip3 install --no-cache-dir -r requirements.txt
 
 COPY . .
 
-# Pre-warm the Lean + Mathlib environment so the first user request isn't slow.
-# Runs lean_interact with Mathlib once during the Docker build, triggering
-# Mathlib cache population. Failures are tolerated so the image still builds.
-RUN python3 -c "import sys; sys.path.insert(0, '/app/src'); from lean_verifier import LeanEnvironment; env = LeanEnvironment(use_mathlib=True); env.verify_proof('import Mathlib\n\n#check Nat.add_comm'); env.close()" \
-    || echo "Lean warm-up skipped (non-fatal)"
-
 EXPOSE 7860
 ENV GRADIO_SERVER_NAME=0.0.0.0