---
license: apache-2.0
language:
- en
tags:
- theorem-proving
- lean4
- conjecture-generation
- gguf
- ollama
- ravenx
- conjecturebench
- prediction-markets
- trading
- polymarket
- formal-verification
base_model: Qwen/Qwen3-8B
datasets:
- AI-MO/NuminaMath-LEAN
pipeline_tag: text-generation
---

# RavenX-Conjecture-Qwen3-8B-GGUF

**The first conjecture generation model fine-tuned on MLX for Apple Silicon. GGUF Q8_0 for Ollama / llama.cpp / LM Studio.**

Built by a security AI company that doesn't do math. That's the point.

## Quick Start

```bash
ollama run hf.co/deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF
llama-cli -m RavenX-Conjecture-Qwen3-8B-Q8_0.gguf --conversation -ngl 99
```

## The Story

On July 22, 2026 — first day back after two weeks sick — RavenX AI Labs:

1. Read the ConjectureBench paper (arXiv:2510.11986) — nobody had implemented it locally
2. Built the first MLX-native LEAN-FIRE pipeline on Apple Silicon
3. Fine-tuned the first conjecture generation model that exists
4. 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

```
SYSTEM: You are a formal verification expert. Your task is to PROVE a conjecture is true.
Process: 1) DECOMPOSE into atomic claims 2) FORMALIZE in Lean 4 3) EVIDENCE for each claim
4) SYNTHESIZE proof 5) CONFIDENCE rating (0-1).
Output: decomposition, formal statement, proof sketch, verdict (PROVED / LIKELY TRUE /
INSUFFICIENT EVIDENCE), weakest link.

USER: Every even integer greater than 2 is the sum of two primes (Goldbach's conjecture)
/no_think
```

### Mode 2: BREAK — Find a Counterexample

This is how we verified the DGG counterexample:

```
SYSTEM: You are a counterexample hunter. Your task is to DISPROVE a conjecture.
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.
Key: exhaustive verification, integer arithmetic, show all work.

USER: 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.
Try: small planar graphs, 3 terminals, unequal demands, razor-thin margins.
/no_think
```

### Mode 3: PREDICT — Trading, Polymarket, Security

**The killer app.** Conjecture = Prediction. Formalization = Resolution criteria. Counterexample = The trade.

```
SYSTEM: You are a prediction engine. A prediction IS a conjecture. Resolution criteria IS
verification. 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).
Use Kelly criterion for position sizing. State max downside.

USER: **Claim:** BTC will close above $100,000 by September 30, 2026
**Current Market Price:** 0.35
**Implied Probability:** 35.0%
**Context:** Current price ~$68K. ETF inflows $200M/day. Halving April 2024. Fed cutting Q3.
/no_think
```

### Security Conjecture

```
SYSTEM: You are a security verification engine. Formalize vulnerabilities as formal claims,
then prove or disprove. Process: 1) FORMALIZE the vulnerability 2) ATTACK MODEL 3) Check CVE/NVD
4) Construct minimal PoC 5) Prove or disprove 6) Responsible disclosure if confirmed.

USER: The Sovereignty Chain's gradient ledger encryption prevents extraction of fine-tuning
data without the owner's private key. Attacker has full model weights but not the PGP key.
/no_think
```

---

## 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

```bash
git clone https://github.com/DeadByDawn101/ravenx-conjecturebench
python formal_verification/verify_dgg.py
```

All 8 routings. Integer arithmetic. 60 > 58. 245-line Lean 4 formalization included.

## Formats

| Format | Size | Link |
|--------|------|------|
| **GGUF Q8_0 (this repo)** | 8.1 GB | You're here |
| MLX (safetensors) | 4.3 GB | [MLX version](https://huggingface.co/deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX) |

## Full Pipeline + Universal Prompt Engine

[github.com/DeadByDawn101/ravenx-conjecturebench](https://github.com/DeadByDawn101/ravenx-conjecturebench)

Includes `prompts/universal_conjecture.py` — run predictions from the command line:
```bash
python prompts/universal_conjecture.py --mode predict --domain trading --claim "BTC > 100K by Sept" --market-price 0.35 --run
python prompts/universal_conjecture.py --mode break --claim "Your conjecture here" --run
python prompts/universal_conjecture.py --example dgg_break --run
```

## RavenX AI Labs

155K+ HF downloads | 22 models | 2 USPTO patents | Security AI

- [CyberAgent-35B](https://huggingface.co/deadbydawn101/RavenX-CyberAgent-Qwen3.6-35B-A3B-Opus-4.7-OpenMythos-Pentester-BugHunter-RATH-GGUF) — 20K+ downloads
- [Gemma-4-E4B](https://huggingface.co/deadbydawn101/gemma-4-E4B-Agentic-Opus-Reasoning-GeminiCLI-mlx-4bit) — 103K+ downloads

[@DeadByDawn101](https://github.com/DeadByDawn101) | [@RavenXllm](https://x.com/RavenXllm)

*"We don't do math. That's the point." — RavenX AI Labs*