Sovereign Models and GGUFs
Collection
Small, local-first language models. Nemotron fine-tunes, reward models, deterministic routing, and GGUF exports. Everything runs on consumer GPUs. • 24 items • Updated
Source: github.com/SNAPKITTYWEST/hilbert
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 · BSL-1.1 / AGPL-3.0 · Patent Pending — Bel Esprit D'Accord Irrevocable Trust
Download
Via Ollama:
ollama run jessicalw34/HILBERT
GGUF weights: Snapkitty/snapkitty-nemotron — snapkitty-nemotron.Q4_K_M.gguf
License
Licensed under SnapKitty Tri-License. Full text: LICENSE.tri.
💼 Commercial License
Snapkitty code is free and open under AGPL-3.0 for open-source use. Building a commercial product or service? A proprietary commercial license from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.
Inference Providers NEW
This model isn't deployed by any Inference Provider. 🙋 Ask for provider support