Sync with GitHub, license metadata from LICENSE files, commercial license notice
Browse files
README.md
CHANGED
|
@@ -1,66 +1,81 @@
|
|
| 1 |
-
---
|
| 2 |
-
license: other
|
| 3 |
-
license_name:
|
| 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 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
---
|
| 2 |
+
license: other
|
| 3 |
+
license_name: snapkitty-tri-license
|
| 4 |
+
license_link: https://huggingface.co/Snapkitty/hilbert/blob/main/LICENSE.tri
|
| 5 |
+
tags:
|
| 6 |
+
- snapkitty
|
| 7 |
+
- sovereign-compute
|
| 8 |
+
- gguf
|
| 9 |
+
- ollama
|
| 10 |
+
- agent
|
| 11 |
+
language:
|
| 12 |
+
- en
|
| 13 |
+
---
|
| 14 |
+
|
| 15 |
+
> Source: [github.com/SNAPKITTYWEST/hilbert](https://github.com/SNAPKITTYWEST/hilbert)
|
| 16 |
+
|
| 17 |
+
# HILBERT
|
| 18 |
+
|
| 19 |
+
**SnapKitty Research & Proof Agent**
|
| 20 |
+
|
| 21 |
+
HILBERT is the formal verification and deep reasoning model in the SnapKitty TORUS/NULL/HILBERT routing stack.
|
| 22 |
+
|
| 23 |
+
Named for David Hilbert β who attempted to formalize all of mathematics.
|
| 24 |
+
|
| 25 |
+
## Role
|
| 26 |
+
|
| 27 |
+
HILBERT handles: mathematics, formal proofs, Lean 4, ISA design, complex reasoning, anything that requires depth over speed.
|
| 28 |
+
|
| 29 |
+
Routed to by TORUS (Gemma) when a task requires rigor.
|
| 30 |
+
|
| 31 |
+
## Stack
|
| 32 |
+
|
| 33 |
+
```
|
| 34 |
+
Input
|
| 35 |
+
β
|
| 36 |
+
TORUS (orchestrator) β routes here for hard problems
|
| 37 |
+
β
|
| 38 |
+
HILBERT (this model) β proves, verifies, reasons
|
| 39 |
+
β
|
| 40 |
+
QUANTUMAP β hallucination gate
|
| 41 |
+
β
|
| 42 |
+
WORM seal
|
| 43 |
+
```
|
| 44 |
+
|
| 45 |
+
## Constitution
|
| 46 |
+
|
| 47 |
+
- Formal proofs in Lean 4. Zero sorry terms.
|
| 48 |
+
- Math is the source of truth. Text is just a shadow of it.
|
| 49 |
+
- Entropy bound H β€ 0.20 enforced on all outputs.
|
| 50 |
+
- No hallucination. If unproven, say so explicitly.
|
| 51 |
+
- SystemVerilog RTL for hardware. Mathematical notation for theory.
|
| 52 |
+
|
| 53 |
+
## Base
|
| 54 |
+
|
| 55 |
+
Built on `snapkitty-nemotron` β fine-tuned Nemotron for the SnapKitty sovereign stack.
|
| 56 |
+
|
| 57 |
+
## Part of
|
| 58 |
+
|
| 59 |
+
[SnapKitty](https://github.com/SNAPKITTYWEST) Β· BSL-1.1 / AGPL-3.0 Β· Patent Pending β Bel Esprit D'Accord Irrevocable Trust
|
| 60 |
+
|
| 61 |
+
|
| 62 |
+
## Download
|
| 63 |
+
|
| 64 |
+
**Via Ollama:**
|
| 65 |
+
```bash
|
| 66 |
+
ollama run jessicalw34/HILBERT
|
| 67 |
+
```
|
| 68 |
+
|
| 69 |
+
**GGUF weights:** [Snapkitty/snapkitty-nemotron β `snapkitty-nemotron.Q4_K_M.gguf`](https://huggingface.co/Snapkitty/snapkitty-nemotron)
|
| 70 |
+
|
| 71 |
+
---
|
| 72 |
+
|
| 73 |
+
## License
|
| 74 |
+
|
| 75 |
+
Licensed under **SnapKitty Tri-License**. Full text: [LICENSE.tri](LICENSE.tri).
|
| 76 |
+
|
| 77 |
+
### πΌ Commercial License
|
| 78 |
+
|
| 79 |
+
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.
|
| 80 |
+
|
| 81 |
+
**[β Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20hilbert)** Β· A.parr@belespritdaccord.uk
|