File size: 1,595 Bytes
729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 729eb92 d732114 ef7e7f9 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 | ---
license: other
license_name: sovereign-source-license-v2
tags:
- snapkitty
- sovereign-compute
- gguf
- ollama
- agent
language:
- en
---
# HILBERT
**SnapKitty Research & Proof Agent**
HILBERT is the formal verification and deep reasoning model in the SnapKitty TORUS/NULL/HILBERT routing stack.
Named for David Hilbert — who attempted to formalize all of mathematics.
## Role
HILBERT handles: mathematics, formal proofs, Lean 4, ISA design, complex reasoning, anything that requires depth over speed.
Routed to by TORUS (Gemma) when a task requires rigor.
## Stack
```
Input
↓
TORUS (orchestrator) — routes here for hard problems
↓
HILBERT (this model) — proves, verifies, reasons
↓
QUANTUMAP — hallucination gate
↓
WORM seal
```
## Constitution
- Formal proofs in Lean 4. Zero sorry terms.
- Math is the source of truth. Text is just a shadow of it.
- Entropy bound H ≤ 0.20 enforced on all outputs.
- No hallucination. If unproven, say so explicitly.
- SystemVerilog RTL for hardware. Mathematical notation for theory.
## Base
Built on `snapkitty-nemotron` — fine-tuned Nemotron for the SnapKitty sovereign stack.
## Part of
[SnapKitty](https://github.com/SNAPKITTYWEST) · BSL-1.1 / AGPL-3.0 · Patent Pending — Bel Esprit D'Accord Irrevocable Trust
## Download
**Via Ollama:**
```bash
ollama run jessicalw34/HILBERT
```
**GGUF weights:** [Snapkitty/snapkitty-nemotron — `snapkitty-nemotron.Q4_K_M.gguf`](https://huggingface.co/Snapkitty/snapkitty-nemotron)
|