Model card: first MLX conjecture model

README.md

@@ -1,9 +1,88 @@
 ---
-library_name: mlx
 license: apache-2.0
-license_link: https://huggingface.co/Qwen/Qwen3-8B/blob/main/LICENSE
-pipeline_tag: text-generation
-base_model: mlx-community/Qwen3-8B-4bit
+language:
+- en
+library_name: mlx
 tags:
+- theorem-proving
+- lean4
+- conjecture-generation
+- apple-silicon
 - mlx
+- ravenx
+base_model: Qwen/Qwen3-8B
+datasets:
+- AI-MO/NuminaMath-LEAN
+pipeline_tag: text-generation
 ---
+
+# 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:
+
+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.
+
+## 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 vs After
+
+**Putnam 2004 A1** (existence proof): Before = no output. After = correct existential Lean structure.
+
+**Putnam 2013 B2** (cosine max = 3): Before = no output. After = IsGreatest with Finset.range, Real.pi (correct Mathlib idioms).
+
+## Usage
+
+```python
+from mlx_lm import load, generate
+model, tokenizer = load("deadbydawn101/RavenX-Conjecture-Qwen3-8B-MLX")
+prompt = tokenizer.apply_chat_template([
+    {"role": "system", "content": "You are an expert mathematician. Generate the precise solution as a Lean 4 expression."},
+    {"role": "user", "content": "What are the real roots of x^2 - 4x = 0?\n/no_think"},
+], tokenize=False, add_generation_prompt=True)
+output = generate(model, tokenizer, prompt=prompt, max_tokens=512)
+```
+
+## 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. Lean 4 formalization (245 lines) included.
+
+## Formats
+
+| Format | Size | Link |
+|--------|------|------|
+| **MLX (this repo)** | 4.3 GB | You're here |
+| GGUF Q8_0 | 8.1 GB | [GGUF](https://huggingface.co/deadbydawn101/RavenX-Conjecture-Qwen3-8B-GGUF) |
+
+Pipeline: [github.com/DeadByDawn101/ravenx-conjecturebench](https://github.com/DeadByDawn101/ravenx-conjecturebench)
+
+## RavenX AI Labs
+
+155K+ HF downloads | 22 models | 2 USPTO patents | Security AI
+
+*"We don't do math. That's the point." — RavenX AI Labs*