---
license: agpl-3.0
language:
- en
tags:
- formal-mathematics
- theorem-proving
- lean4
- attention-mechanism
- nand-decomposition
- snapkitty
- research
- latex
pretty_name: SnapKitty Formal Papers
---

# papers

Formal mathematics papers from the SnapKitty / SNAPKITTYWEST research stack.

## Contents

- `formal-math/attention_nand_decomposition_full.pdf` — Full NAND decomposition of the attention mechanism
- `formal-math/gkn_boole_e7_quartic.pdf` — GKN Boole E7 quartic (PDF + LaTeX source)
- `formal-math/theorem_t1.pdf` through `theorem_t4.pdf` — Core theorem sequence

## Links

- [SNAPKITTYWEST GitHub](https://github.com/SNAPKITTYWEST)
- [sov-kernel-monster](https://huggingface.co/Snapkitty/sov-kernel-monster)

---

## License

Licensed under **AGPL-3.0**. Full text: [LICENSE](LICENSE).

### 💼 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.

**[→ Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20snapkitty-papers)** · A.parr@belespritdaccord.uk