mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
b038778361
- SDPVerify.lean: certificate verification engine (714 lines, compiles cleanly) - GoormaghtighCert.lean: Goormaghtigh conjecture SDP certificate - HachimojiManifoldAxiom/HachimojiSubstitution: Hachimoji DNA encoding - GeneticBraidBridge.lean: genetic algorithm braid bridge - load_dependency_graph/load_module_graph: Gremlin Cosmos DB graph loaders - test_graph_queries/rrc_math_xref: graph verification queries - Gremlin mathblob DB provisioned and accessible - Branch cleanup: deleted 11 stale remote branches Build: 3297 jobs, 0 errors (lake build Semantics.SDPVerify)
97 lines
4.1 KiB
Markdown
97 lines
4.1 KiB
Markdown
---
|
||
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', ''))
|
||
```
|