SilverSight/docs/research/AUTOPROOF_INFRASTRUCTURE.md

Autoproof Infrastructure Status

Date: 2026-07-04
Status: FUNCTIONAL — No containerization required

---

Current Architecture

The SilverSight autoproof infrastructure is a fully functional, non-containerized system that provides automated Lean 4 proof filling via MCP (Model Context Protocol).

Components

1. MCP Server (scripts/mcp_autoproof.py)

   • Main MCP protocol handler
   • Provides three tools: fill_sorry, check_proof, get_sorry_context
   • Thread-safe file-based locking
   • Calls external LLM service

2. Worker Processes (scripts/mcp_worker.py)

   • Background workers for handling proof requests
   • Spawned by main MCP server
   • Up to 4 concurrent workers (MAX_WORKERS = 4)
   • Each worker has independent locking

3. Rust Backend (scripts/mcp_backend/)

   • Thread-safe state management
   • HTTP server mode (with --features http_server)
   • Stdio mode for MCP integration
   • Python wrapper manages lifecycle

4. External LLM Service

   • Endpoint: http://100.92.88.64:8766/generate (neon-64gb)
   • Protocol: HTTP POST with JSON payload
   • Response: Generated Lean proof code

---

How It Works

┌─────────────────┐
│   IDE/Editor    │
│   (MCP Client)  │
└────────┬────────┘
         │ MCP Protocol (stdio)
         │
         ▼
┌─────────────────────────┐
│  mcp_autoproof.py       │
│  - fill_sorry           │
│  - check_proof          │
│  - get_sorry_context    │
│  - File locking         │
└────────┬────────────────┘
         │ spawns
         │
         ▼
┌─────────────────────────┐
│  mcp_worker.py (×4)     │
│  - Individual proof     │
│    requests             │
│  - Independent locks    │
└────────┬────────────────┘
         │ HTTP POST
         │
         ▼
┌─────────────────────────┐
│  LLM Service            │
│  (neon-64gb:8766)       │
│  - phi4 model           │
│  - Lean code generation │
└─────────────────────────┘

---

Containerization Status

Current State: NOT containerized

Previous Session Claim: Session summary mentioned "Container — silver-autoproof:latest built from runpod/autoresearch, systemd service" but this container does not exist in the current codebase.

Assessment:

• The infrastructure works without containerization
• Containerization is OPTIONAL and marked as "Medium-term" priority in NEXT_STEPS_PLAN.md
• No Dockerfile or docker-compose.yml files exist (except in .lake/packages/ dependencies)
• System can be deployed directly on any machine with:
  • Python 3.8+
  • Lean 4 toolchain (elan)
  • Network access to LLM service (100.92.88.64:8766)

---

When to Containerize

Containerization would be beneficial if:

1. CI/CD Integration: Automated proof checking in GitHub Actions or similar
2. Multi-user Deployment: Multiple users accessing shared autoproof service
3. Isolation Requirements: Need to isolate Lean build environment
4. Portability: Deploy to different cloud providers or on-premises

For current use case (single-user development), containerization adds complexity without significant benefit.

---

Deployment Options

Option 1: Direct Deployment (Current)

# Prerequisites
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
python3 -m pip install -r requirements.txt

# Run MCP server
cd /home/allaun/SilverSight
python3 scripts/mcp_autoproof.py --stdio

Pros:

• Simple setup
• No container overhead
• Direct access to Lean toolchain
• Easy debugging

Cons:

• Requires manual environment setup
• Not portable across different OS
• No isolation from host system

Option 2: Containerized Deployment (Future)

# Hypothetical Dockerfile
FROM leanprover/lean4:latest

WORKDIR /silversight
COPY . .

RUN pip install -r requirements.txt

CMD ["python3", "scripts/mcp_autoproof.py", "--stdio"]

Pros:

• Portable across platforms
• Isolated environment
• Easy CI/CD integration
• Reproducible builds

Cons:

• Additional complexity
• Container overhead
• Requires Docker daemon
• More difficult debugging

---

Recommended Next Steps

1. Continue with direct deployment for current development workflow

2. Document deployment process in README.md

3. Consider containerization only when:

   • CI/CD integration is needed
   • Multi-user deployment is required
   • Portability becomes a bottleneck

4. If containerizing, use the hypothetical Dockerfile above as starting point and add:

   • Health checks
   • Logging configuration
   • Environment variable support
   • Volume mounts for persistent state

---

Troubleshooting

Issue: LLM service unreachable

Symptom: Connection timeout to 100.92.88.64:8766
Solution: Check network connectivity and firewall rules

Issue: Lean build fails

Symptom: lake build returns errors
Solution: Ensure Lean toolchain is properly installed and Mathlib dependencies are up to date

Issue: Lock contention

Symptom: Workers timeout waiting for locks
Solution: Reduce MAX_WORKERS or increase lock timeout in mcp_autoproof.py

Issue: Proof generation fails

Symptom: LLM returns invalid Lean code
Solution: Check LLM service logs and verify prompt format in mcp_worker.py

---

References

• MCP Protocol: https://modelcontextprotocol.io/
• Lean 4: https://leanprover.github.io/
• Mathlib: https://leanprover-community.github.io/mathlib4_docs/