---
name: research-stack-workflow
description: "Token-efficient Lean proof workflow for Research Stack — route to neon CPU (0 token cost), use ContextStream for context, call token-saver MCP for builds."
---

# Research Stack — Token-Efficient Proof Workflow

## Core Principle
**Free local compute first.** Neon server (100.92.88.64) runs Ollama with DeepSeek-Prover-V2-7B and Goedel-Prover-V2-8B on CPU — zero API tokens consumed. Only fall back to paid APIs when local inference fails.

## Session Protocol (Every Message)

| Step | Action | Tool Call | Token Cost |
|------|--------|-----------|------------|
| 1 | Get context | `context(user_message="...", format="minified", max_tokens=200)` | ~200 |
| 2 | Search first | `search(mode="auto", query="...")` before Glob/Grep | ~50 |
| 3 | Use token-saver | `token-saver__verify_build(module=...)` | **0** |
| 4 | Generate proof | `token-saver__generate_proof(context=...)` → neon CPU | **0** |
| 5 | Fallback | Only if token-saver returns error → use paid MCP | varies |

## Proof Generation Pipeline

```
1. context(user_message="need proof for theorem X")    # get relevant context (~200 tokens)
2. search(mode="auto", query="theorem X sidon")        # find related proofs (~50 tokens)
3. token-saver__generate_proof(theorem_context=...)      # neon DeepSeek-Prover (0 tokens)
4. token-saver__compile_check(code=...)                  # verify compilation (0 tokens)
5. token-saver__verify_build(module=...)                 # full lake build (0 tokens)
```

## Available MCP Servers (30 total)

### Free Local (0 tokens)
| Server | Tools | Backend |
|--------|-------|---------|
| `token-saver` | verify_build, compile_check, generate_proof, doc_lookup, format_code, linter_check, classify_proof | neon CPU + qfox-1 |
| `lean-lsp` | Lean type-checking, proof info | local |
| `lean` | lake build via lean-mcp-server | local |
| `git` | git history, blame, diff | local |
| `filesystem` | file read/write | local |
| `fetch` | HTTP fetch for docs | local |
| `sympy` | symbolic math verification | local |
| `context7` | live library docs | local |
| `shape-index` | 112K theorem shape index | local |

### Cloud (token cost)
| Server | Use Case |
|--------|----------|
| `contextstream` | Persistent memory, context, search |
| `github` | PRs, issues, CI status |
| `arxiv` | Paper search |
| `remote-lean-proof` | AWS proof server fallback |

## Cached Instructions (auto-injected)

```
Research Stack context:
- 30 MCP servers registered in .mcp.json
- TopologicalBraidAdapter proofs: COMPLETED
- Active target: E8Sidon.lean (E₈ Sidon framework, 1657 lines)
- Quarantined: HybridTSMPISTTorus.lean (geneticScoreBounded theorem)
- token-saver MCP provides free compute on neon CPU
- Route proof generation through neon before paid fallback
- call context(user_message=...) at start of EVERY response
- call search(mode="auto") before Glob/Grep/Read
```

## Neon Server Details

| Property | Value |
|----------|-------|
| URL | http://100.92.88.64:11434 |
| Models | DeepSeek-Prover-V2-7B, Goedel-Prover-V2-8B, Qwen3.6-35B |
| Inference | CPU-only, 18 threads, 0 tokens |
| Build Server | http://100.88.57.96:8765 (if running) |

## Lessons (from ContextStream)

- ℕ/ℤ/ℚ/ℝ unicode notations unavailable in Semantics.Toolkit-only files
- `open Classical` + `haveI DecidableRel` = two conflicting instances → whnf timeout
- `set_option` directives must come AFTER all import statements
- OTM provability doctrine: every statement provable, rooted in named theorems

## Quick Reference

```bash
# Test neon connectivity
curl -s http://100.92.88.64:11434/api/tags

# Generate proof via token-saver (0 tokens)
python3 -c "
import json, urllib.request
body = json.dumps({'model': 'hf.co/irmma/DeepSeek-Prover-V2-7B-Q4_K_M-GGUF', 'prompt': 'theorem test := by', 'raw': True, 'stream': False, 'options': {'temperature': 0}}).encode()
req = urllib.request.Request('http://100.92.88.64:11434/api/generate', data=body, headers={'Content-Type': 'application/json'}, method='POST')
with urllib.request.urlopen(req, timeout=300) as resp:
    print(json.loads(resp.read()).get('response', ''))
```