Instructions to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Notebooks
Google Colab
Kaggle
Local Apps Settings

How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with llama.cpp:

Install (macOS, Linux)

curl -LsSf https://llama.app/install.sh | sh
# Start a local OpenAI-compatible server with a web UI:
llama serve -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0
# Run inference directly in the terminal:
llama cli -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

Install from WinGet (Windows)

winget install llama.cpp
# Start a local OpenAI-compatible server with a web UI:
llama serve -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0
# Run inference directly in the terminal:
llama cli -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

Use pre-built binary

# Download pre-built binary from:
# https://github.com/ggerganov/llama.cpp/releases
# Start a local OpenAI-compatible server with a web UI:
./llama-server -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0
# Run inference directly in the terminal:
./llama-cli -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

Build from source code

git clone https://github.com/ggerganov/llama.cpp.git
cd llama.cpp
cmake -B build
cmake --build build -j --target llama-server llama-cli
# Start a local OpenAI-compatible server with a web UI:
./build/bin/llama-server -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0
# Run inference directly in the terminal:
./build/bin/llama-cli -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

Use Docker

docker model run hf.co/deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

LM Studio
Jan

vLLM

How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

Ollama
How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with Ollama:
```
ollama run hf.co/deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0
```

Unsloth Studio

How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with Unsloth Studio:

Install Unsloth Studio (macOS, Linux, WSL)

curl -fsSL https://unsloth.ai/install.sh | sh
# Run unsloth studio
unsloth studio -H 0.0.0.0 -p 8888
# Then open http://localhost:8888 in your browser
# Search for deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF to start chatting

Install Unsloth Studio (Windows)

irm https://unsloth.ai/install.ps1 | iex
# Run unsloth studio
unsloth studio -H 0.0.0.0 -p 8888
# Then open http://localhost:8888 in your browser
# Search for deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF to start chatting

Using HuggingFace Spaces for Unsloth

# No setup required
# Open https://huggingface.co/spaces/unsloth/studio in your browser
# Search for deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF to start chatting

How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with Pi:

Start the llama.cpp server

# Install llama.cpp:
brew install llama.cpp
# Start a local OpenAI-compatible server:
llama serve -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

Configure the model in Pi

# Install Pi:
npm install -g @mariozechner/pi-coding-agent
# Add to ~/.pi/agent/models.json:
{
  "providers": {
    "llama-cpp": {
      "baseUrl": "http://localhost:8080/v1",
      "api": "openai-completions",
      "apiKey": "none",
      "models": [
        {
          "id": "deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0"
        }
      ]
    }
  }
}

Run Pi

# Start Pi in your project directory:
pi

OpenClaw new

How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with OpenClaw:

Start the llama.cpp server

# Install llama.cpp:
brew install llama.cpp
# Start a local OpenAI-compatible server:
llama serve -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

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-GGUF:Q8_0" \
  --custom-provider-id llama-cpp \
  --custom-compatibility openai \
  --custom-text-input \
  --accept-risk \
  --skip-health

Run OpenClaw

openclaw agent --local --agent main --message "Hello from Hugging Face"

Docker Model Runner
How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with Docker Model Runner:
```
docker model run hf.co/deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0
```

Lemonade

How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with Lemonade:

Pull the model

# Download Lemonade from https://lemonade-server.ai/
lemonade pull deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

Run and chat with the model

lemonade run user.RavenX-Conjecture-Qwen3-8B-GGUF-Q8_0

List all available models

lemonade list

Hermes Agent

How to use deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF with Hermes Agent:

Start the llama.cpp server

# Install llama.cpp:
brew install llama.cpp
# Start a local OpenAI-compatible server:
llama serve -hf deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF:Q8_0

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-GGUF:Q8_0

Run Hermes

hermes

Atomic Chat

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

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:

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

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

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

Full Pipeline + Universal Prompt Engine

github.com/DeadByDawn101/ravenx-conjecturebench

Includes prompts/universal_conjecture.py — run predictions from the command line:

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 — 20K+ downloads
Gemma-4-E4B — 103K+ downloads

@DeadByDawn101 | @RavenXllm

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

Downloads last month: 204

GGUF

Model size

8B params

Architecture

qwen3

Hardware compatibility

8-bit

Model tree for deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF

Base model

Qwen/Qwen3-8B-Base

Finetuned

Qwen/Qwen3-8B

Quantized

(374)

this model

Dataset used to train deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF

Paper for deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF

Conjecturing: An Overlooked Step in Formal Mathematical Reasoning

Paper • 2510.11986 • Published Oct 13, 2025