| name |
description |
| research-stack-workflow |
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
Lessons (from ContextStream)
- ℕ/ℤ/ℚ/ℝ unicode notations unavailable in Semantics.Toolkit-only files
open Classical + haveI DecidableRel = two conflicting instances → whnf timeoutset_option directives must come AFTER all import statements- OTM provability doctrine: every statement provable, rooted in named theorems
Quick Reference
# 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', ''))
allaun
b038778361