Text Generation
MLX
Safetensors
English
qwen3
theorem-proving
lean4
conjecture-generation
apple-silicon
ravenx
conjecturebench
prediction-markets
trading
polymarket
formal-verification
conversational
4-bit precision
Instructions to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX with libraries, inference providers, notebooks, and local apps. Follow these links to get started.
- Libraries
- MLX
How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX with MLX:
# Make sure mlx-lm is installed # pip install --upgrade mlx-lm # Generate text with mlx-lm from mlx_lm import load, generate model, tokenizer = load("deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX") prompt = "Write a story about Einstein" messages = [{"role": "user", "content": prompt}] prompt = tokenizer.apply_chat_template( messages, add_generation_prompt=True ) text = generate(model, tokenizer, prompt=prompt, verbose=True) - Notebooks
- Google Colab
- Kaggle
- Local Apps Settings
- LM Studio
- Pi
How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX with Pi:
Start the MLX server
# Install MLX LM: uv tool install mlx-lm # Start a local OpenAI-compatible server: mlx_lm.server --model "deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX"
Configure the model in Pi
# Install Pi: npm install -g @earendil-works/pi-coding-agent # Add to ~/.pi/agent/models.json: { "providers": { "mlx-lm": { "baseUrl": "http://localhost:8080/v1", "api": "openai-completions", "apiKey": "none", "models": [ { "id": "deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX" } ] } } }Run Pi
# Start Pi in your project directory: pi
- MLX LM
How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX with MLX LM:
Generate or start a chat session
# Install MLX LM uv tool install mlx-lm # Interactive chat REPL mlx_lm.chat --model "deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX"
Run an OpenAI-compatible server
# Install MLX LM uv tool install mlx-lm # Start the server mlx_lm.server --model "deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX" # Calling the OpenAI-compatible server with curl curl -X POST "http://localhost:8000/v1/chat/completions" \ -H "Content-Type: application/json" \ --data '{ "model": "deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX", "messages": [ {"role": "user", "content": "Hello"} ] }' - Hermes Agent
How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX with Hermes Agent:
Start the MLX server
# Install MLX LM: uv tool install mlx-lm # Start a local OpenAI-compatible server: mlx_lm.server --model "deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX"
Configure Hermes
# Install Hermes: curl -fsSL https://hermes-agent.nousresearch.com/install.sh | bash hermes setup # Point Hermes at the local server: hermes config set model.provider custom hermes config set model.base_url http://127.0.0.1:8080/v1 hermes config set model.default deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX
Run Hermes
hermes
- Atomic Chat
- OpenClaw
How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX with OpenClaw:
Start the MLX server
# Install MLX LM: uv tool install mlx-lm # Start a local OpenAI-compatible server: mlx_lm.server --model "deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX"
Configure OpenClaw
# Install OpenClaw: npm install -g openclaw@latest # Register the local server and set it as the default model: openclaw onboard --non-interactive --mode local \ --auth-choice custom-api-key \ --custom-base-url http://127.0.0.1:8080/v1 \ --custom-model-id "deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX" \ --custom-provider-id mlx-lm \ --custom-compatibility openai \ --custom-text-input \ --accept-risk \ --skip-health
Run OpenClaw
openclaw agent --local --agent main --message "Hello from Hugging Face"
v2: Universal Conjecture Engine prompts baked in (validate/break/predict)
Browse files
README.md
CHANGED
|
@@ -10,6 +10,11 @@ tags:
|
|
| 10 |
- apple-silicon
|
| 11 |
- mlx
|
| 12 |
- ravenx
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 13 |
base_model: Qwen/Qwen3-8B
|
| 14 |
datasets:
|
| 15 |
- AI-MO/NuminaMath-LEAN
|
|
@@ -33,6 +38,82 @@ On July 22, 2026 β first day back after two weeks sick β RavenX AI Labs:
|
|
| 33 |
|
| 34 |
We don't do math. We do security AI and sovereign infrastructure. We built this cold.
|
| 35 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 36 |
## Training
|
| 37 |
|
| 38 |
| Parameter | Value |
|
|
@@ -45,23 +126,10 @@ We don't do math. We do security AI and sovereign infrastructure. We built this
|
|
| 45 |
| Time | ~75 min on Apple M4 Max 128GB |
|
| 46 |
| Tokens trained | 1,010,330 |
|
| 47 |
|
| 48 |
-
## Results
|
| 49 |
-
|
| 50 |
-
**Putnam 2004 A1** (existence proof): Before = no output. After = correct existential Lean structure.
|
| 51 |
-
|
| 52 |
-
**Putnam 2013 B2** (cosine max = 3): Before = no output. After = IsGreatest with Finset.range, Real.pi (correct Mathlib idioms).
|
| 53 |
|
| 54 |
-
|
| 55 |
-
|
| 56 |
-
```python
|
| 57 |
-
from mlx_lm import load, generate
|
| 58 |
-
model, tokenizer = load("deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX")
|
| 59 |
-
prompt = tokenizer.apply_chat_template([
|
| 60 |
-
{"role": "system", "content": "You are an expert mathematician. Generate the precise solution as a Lean 4 expression."},
|
| 61 |
-
{"role": "user", "content": "What are the real roots of x^2 - 4x = 0?\n/no_think"},
|
| 62 |
-
], tokenize=False, add_generation_prompt=True)
|
| 63 |
-
output = generate(model, tokenizer, prompt=prompt, max_tokens=512)
|
| 64 |
-
```
|
| 65 |
|
| 66 |
## DGG Conjecture β Verify Yourself
|
| 67 |
|
|
@@ -70,7 +138,7 @@ git clone https://github.com/DeadByDawn101/ravenx-conjecturebench
|
|
| 70 |
python formal_verification/verify_dgg.py
|
| 71 |
```
|
| 72 |
|
| 73 |
-
All 8 routings. Integer arithmetic. 60 > 58. Lean 4 formalization
|
| 74 |
|
| 75 |
## Formats
|
| 76 |
|
|
@@ -79,10 +147,24 @@ All 8 routings. Integer arithmetic. 60 > 58. Lean 4 formalization (245 lines) in
|
|
| 79 |
| **MLX (this repo)** | 4.3 GB | You're here |
|
| 80 |
| GGUF Q8_0 | 8.1 GB | [GGUF](https://huggingface.co/deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF) |
|
| 81 |
|
| 82 |
-
Pipeline
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 83 |
|
| 84 |
## RavenX AI Labs
|
| 85 |
|
| 86 |
155K+ HF downloads | 22 models | 2 USPTO patents | Security AI
|
| 87 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 88 |
*"We don't do math. That's the point." β RavenX AI Labs*
|
|
|
|
| 10 |
- apple-silicon
|
| 11 |
- mlx
|
| 12 |
- ravenx
|
| 13 |
+
- conjecturebench
|
| 14 |
+
- prediction-markets
|
| 15 |
+
- trading
|
| 16 |
+
- polymarket
|
| 17 |
+
- formal-verification
|
| 18 |
base_model: Qwen/Qwen3-8B
|
| 19 |
datasets:
|
| 20 |
- AI-MO/NuminaMath-LEAN
|
|
|
|
| 38 |
|
| 39 |
We don't do math. We do security AI and sovereign infrastructure. We built this cold.
|
| 40 |
|
| 41 |
+
---
|
| 42 |
+
|
| 43 |
+
## π₯ Universal Conjecture Engine β 3 Modes, 5 Domains
|
| 44 |
+
|
| 45 |
+
The core insight: **conjecture generation IS prediction.** Same pipeline whether you're breaking a 30-year-old math conjecture or sizing a Polymarket position.
|
| 46 |
+
|
| 47 |
+
| Mode | What It Does |
|
| 48 |
+
|------|-------------|
|
| 49 |
+
| **VALIDATE** | Prove a conjecture true β decompose, formalize, verify |
|
| 50 |
+
| **BREAK** | Find a counterexample β attack surfaces, exhaustive search |
|
| 51 |
+
| **PREDICT** | Generate predictions β trading, Polymarket, security, science |
|
| 52 |
+
|
| 53 |
+
### Mode 1: VALIDATE β Prove It True
|
| 54 |
+
|
| 55 |
+
```python
|
| 56 |
+
from mlx_lm import load, generate
|
| 57 |
+
|
| 58 |
+
model, tokenizer = load("deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX")
|
| 59 |
+
|
| 60 |
+
messages = [
|
| 61 |
+
{"role": "system", "content": """You are a formal verification expert. Your task is to PROVE a conjecture is true.
|
| 62 |
+
Process: 1) DECOMPOSE into atomic claims 2) FORMALIZE in Lean 4 3) EVIDENCE for each claim 4) SYNTHESIZE proof 5) CONFIDENCE rating (0-1).
|
| 63 |
+
Output: decomposition, formal statement, proof sketch, verdict (PROVED / LIKELY TRUE / INSUFFICIENT EVIDENCE), weakest link."""},
|
| 64 |
+
{"role": "user", "content": "Every even integer greater than 2 is the sum of two primes (Goldbach's conjecture)\n/no_think"}
|
| 65 |
+
]
|
| 66 |
+
|
| 67 |
+
prompt = tokenizer.apply_chat_template(messages, tokenize=False, add_generation_prompt=True)
|
| 68 |
+
output = generate(model, tokenizer, prompt=prompt, max_tokens=1024)
|
| 69 |
+
print(output)
|
| 70 |
+
```
|
| 71 |
+
|
| 72 |
+
### Mode 2: BREAK β Find a Counterexample
|
| 73 |
+
|
| 74 |
+
This is how we verified the DGG counterexample. The system prompt that breaks conjectures:
|
| 75 |
+
|
| 76 |
+
```python
|
| 77 |
+
messages = [
|
| 78 |
+
{"role": "system", "content": """You are a counterexample hunter. Your task is to DISPROVE a conjecture.
|
| 79 |
+
Process: 1) FORMALIZE the claim precisely 2) BOUNDARIES β constraints and degrees of freedom 3) ATTACK SURFACE β where is it weakest? 4) CONSTRUCT a candidate 5) VERIFY exhaustively (integer arithmetic) 6) CERTIFY with explicit values.
|
| 80 |
+
Key: exhaustive verification, integer arithmetic, show all work. Beautiful constructions are often correct."""},
|
| 81 |
+
{"role": "user", "content": """For single-source unsplittable flow, every fractional flow can be rounded to unsplittable flow of no higher cost, with each arc's load exceeded by at most d_max.
|
| 82 |
+
|
| 83 |
+
Try: small planar graphs, 3 terminals, unequal demands, razor-thin margins.
|
| 84 |
+
/no_think"""}
|
| 85 |
+
]
|
| 86 |
+
```
|
| 87 |
+
|
| 88 |
+
### Mode 3: PREDICT β Trading, Polymarket, Security
|
| 89 |
+
|
| 90 |
+
**The killer app.** Conjecture = Prediction. Formalization = Resolution criteria. Counterexample = The trade.
|
| 91 |
+
|
| 92 |
+
```python
|
| 93 |
+
# Polymarket prediction
|
| 94 |
+
messages = [
|
| 95 |
+
{"role": "system", "content": """You are a prediction engine. A prediction IS a conjecture. Resolution criteria IS verification.
|
| 96 |
+
Process: 1) FORMALIZE the claim (precise, time-bounded, resolution source) 2) DECOMPOSE into sub-claims with individual probabilities 3) BASE RATE + evidence update 4) COMBINED estimate with confidence interval 5) IDENTIFY THE EDGE (your estimate vs market price).
|
| 97 |
+
Use Kelly criterion for position sizing. State max downside."""},
|
| 98 |
+
{"role": "user", "content": """**Claim:** BTC will close above $100,000 by September 30, 2026
|
| 99 |
+
**Current Market Price:** 0.35
|
| 100 |
+
**Implied Probability:** 35.0%
|
| 101 |
+
**Context:** Current price ~$68K. ETF inflows $200M/day. Halving April 2024. Fed cutting rates Q3 2026.
|
| 102 |
+
/no_think"""}
|
| 103 |
+
]
|
| 104 |
+
|
| 105 |
+
# Security conjecture
|
| 106 |
+
messages = [
|
| 107 |
+
{"role": "system", "content": """You are a security verification engine. Formalize vulnerabilities as formal claims, then prove or disprove.
|
| 108 |
+
Process: 1) FORMALIZE the vulnerability as a claim about system state 2) ATTACK MODEL β attacker capabilities 3) Check CVE/NVD/MITRE 4) Construct minimal PoC 5) Prove or disprove the claim 6) Responsible disclosure if confirmed."""},
|
| 109 |
+
{"role": "user", "content": """The Sovereignty Chain's gradient ledger encryption prevents extraction of fine-tuning data without the owner's private key.
|
| 110 |
+
Context: PGP-based encryption of gradient deltas. Attacker has full model weights but not the PGP key.
|
| 111 |
+
/no_think"""}
|
| 112 |
+
]
|
| 113 |
+
```
|
| 114 |
+
|
| 115 |
+
---
|
| 116 |
+
|
| 117 |
## Training
|
| 118 |
|
| 119 |
| Parameter | Value |
|
|
|
|
| 126 |
| Time | ~75 min on Apple M4 Max 128GB |
|
| 127 |
| Tokens trained | 1,010,330 |
|
| 128 |
|
| 129 |
+
## Results
|
|
|
|
|
|
|
|
|
|
|
|
|
| 130 |
|
| 131 |
+
**Before:** model consumed all tokens in think blocks, no Lean 4 output.
|
| 132 |
+
**After:** correct Lean structures β existential statements, IsGreatest, Finset.range, Real.pi.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 133 |
|
| 134 |
## DGG Conjecture β Verify Yourself
|
| 135 |
|
|
|
|
| 138 |
python formal_verification/verify_dgg.py
|
| 139 |
```
|
| 140 |
|
| 141 |
+
All 8 routings. Integer arithmetic. 60 > 58. 245-line Lean 4 formalization included.
|
| 142 |
|
| 143 |
## Formats
|
| 144 |
|
|
|
|
| 147 |
| **MLX (this repo)** | 4.3 GB | You're here |
|
| 148 |
| GGUF Q8_0 | 8.1 GB | [GGUF](https://huggingface.co/deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF) |
|
| 149 |
|
| 150 |
+
## Full Pipeline + Universal Prompt Engine
|
| 151 |
+
|
| 152 |
+
[github.com/DeadByDawn101/ravenx-conjecturebench](https://github.com/DeadByDawn101/ravenx-conjecturebench)
|
| 153 |
+
|
| 154 |
+
Includes `prompts/universal_conjecture.py` β run predictions from the command line:
|
| 155 |
+
```bash
|
| 156 |
+
python prompts/universal_conjecture.py --mode predict --domain trading --claim "BTC > 100K by Sept" --market-price 0.35 --run
|
| 157 |
+
python prompts/universal_conjecture.py --mode break --claim "Your conjecture here" --run
|
| 158 |
+
python prompts/universal_conjecture.py --example dgg_break --run
|
| 159 |
+
```
|
| 160 |
|
| 161 |
## RavenX AI Labs
|
| 162 |
|
| 163 |
155K+ HF downloads | 22 models | 2 USPTO patents | Security AI
|
| 164 |
|
| 165 |
+
- [CyberAgent-35B](https://huggingface.co/deadbydawn101/RavenX-CyberAgent-Qwen3.6-35B-A3B-Opus-4.7-OpenMythos-Pentester-BugHunter-RATH-GGUF) β 20K+ downloads
|
| 166 |
+
- [Gemma-4-E4B](https://huggingface.co/deadbydawn101/gemma-4-E4B-Agentic-Opus-Reasoning-GeminiCLI-mlx-4bit) β 103K+ downloads
|
| 167 |
+
|
| 168 |
+
[@DeadByDawn101](https://github.com/DeadByDawn101) | [@RavenXllm](https://x.com/RavenXllm)
|
| 169 |
+
|
| 170 |
*"We don't do math. That's the point." β RavenX AI Labs*
|