RavenX-Conjecture-Qwen3-8B-MLX
The first conjecture generation model fine-tuned on MLX for Apple Silicon.
Built by a security AI company that doesn't do math. That's the point.
The Story
On July 22, 2026 — first day back after two weeks sick — RavenX AI Labs:
- Read the ConjectureBench paper (arXiv:2510.11986) — nobody had implemented it locally
- Built the first MLX-native LEAN-FIRE pipeline on Apple Silicon
- Fine-tuned the first conjecture generation model that exists
- Verified Dmitry Rybin's breaking counterexample to the 30-year-old Dinitz-Garg-Goemans conjecture within hours
We don't do math. We do security AI and sovereign infrastructure. We built this cold.
🔥 Universal Conjecture Engine — 3 Modes, 5 Domains
The core insight: conjecture generation IS prediction. Same pipeline whether you're breaking a 30-year-old math conjecture or sizing a Polymarket position.
| Mode | What It Does |
|---|
| VALIDATE | Prove a conjecture true — decompose, formalize, verify |
| BREAK | Find a counterexample — attack surfaces, exhaustive search |
| PREDICT | Generate predictions — trading, Polymarket, security, science |
Mode 1: VALIDATE — Prove It True
1from mlx_lm import load, generate
2
3model, tokenizer = load("deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX")
4
5messages = [
6 {"role": "system", "content": """You are a formal verification expert. Your task is to PROVE a conjecture is true.
7Process: 1) DECOMPOSE into atomic claims 2) FORMALIZE in Lean 4 3) EVIDENCE for each claim 4) SYNTHESIZE proof 5) CONFIDENCE rating (0-1).
8Output: decomposition, formal statement, proof sketch, verdict (PROVED / LIKELY TRUE / INSUFFICIENT EVIDENCE), weakest link."""},
9 {"role": "user", "content": "Every even integer greater than 2 is the sum of two primes (Goldbach's conjecture)\n/no_think"}
10]
11
12prompt = tokenizer.apply_chat_template(messages, tokenize=False, add_generation_prompt=True)
13output = generate(model, tokenizer, prompt=prompt, max_tokens=1024)
14print(output)
Mode 2: BREAK — Find a Counterexample
This is how we verified the DGG counterexample. The system prompt that breaks conjectures:
1messages = [
2 {"role": "system", "content": """You are a counterexample hunter. Your task is to DISPROVE a conjecture.
3Process: 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.
4Key: exhaustive verification, integer arithmetic, show all work. Beautiful constructions are often correct."""},
5 {"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.
6
7Try: small planar graphs, 3 terminals, unequal demands, razor-thin margins.
8/no_think"""}
9]
Mode 3: PREDICT — Trading, Polymarket, Security
The killer app. Conjecture = Prediction. Formalization = Resolution criteria. Counterexample = The trade.
1# Polymarket prediction
2messages = [
3 {"role": "system", "content": """You are a prediction engine. A prediction IS a conjecture. Resolution criteria IS verification.
4Process: 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).
5Use Kelly criterion for position sizing. State max downside."""},
6 {"role": "user", "content": """**Claim:** BTC will close above $100,000 by September 30, 2026
7**Current Market Price:** 0.35
8**Implied Probability:** 35.0%
9**Context:** Current price ~$68K. ETF inflows $200M/day. Halving April 2024. Fed cutting rates Q3 2026.
10/no_think"""}
11]
12
13# Security conjecture
14messages = [
15 {"role": "system", "content": """You are a security verification engine. Formalize vulnerabilities as formal claims, then prove or disprove.
16Process: 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."""},
17 {"role": "user", "content": """The Sovereignty Chain's gradient ledger encryption prevents extraction of fine-tuning data without the owner's private key.
18Context: PGP-based encryption of gradient deltas. Attacker has full model weights but not the PGP key.
19/no_think"""}
20]
Training
| Parameter | Value |
|---|
| Base model | Qwen/Qwen3-8B |
| Method | MLX LoRA (rank 16, alpha 32) |
| Dataset | AI-MO/NuminaMath-LEAN (1,706 train / 190 valid) |
| Iterations | 1,500 |
| Val loss | 2.993 → 0.651 (78% reduction) |
| Time | ~75 min on Apple M4 Max 128GB |
| Tokens trained | 1,010,330 |
Results
Before: model consumed all tokens in think blocks, no Lean 4 output.
After: correct Lean structures — existential statements, IsGreatest, Finset.range, Real.pi.
DGG Conjecture — Verify Yourself
1git clone https://github.com/DeadByDawn101/ravenx-conjecturebench
2python formal_verification/verify_dgg.py
All 8 routings. Integer arithmetic. 60 > 58. 245-line Lean 4 formalization included.
Formats
| Format | Size | Link |
|---|
| MLX (this repo) | 4.3 GB | You're here |
| GGUF Q8_0 | 8.1 GB | GGUF |
Full Pipeline + Universal Prompt Engine
Includes prompts/universal_conjecture.py — run predictions from the command line:
1python prompts/universal_conjecture.py --mode predict --domain trading --claim "BTC > 100K by Sept" --market-price 0.35 --run
2python prompts/universal_conjecture.py --mode break --claim "Your conjecture here" --run
3python prompts/universal_conjecture.py --example dgg_break --run
RavenX AI Labs
155K+ HF downloads | 22 models | 2 USPTO patents | Security AI
- CyberAgent-35B — 20K+ downloads
- Gemma-4-E4B — 103K+ downloads
"We don't do math. That's the point." — RavenX AI Labs
