---
title: Mu
emoji: 🧬
colorFrom: yellow
colorTo: red
sdk: gradio
sdk_version: 6.9.0
app_file: app.py
pinned: false
license: mit
short_description: Lean-verified ML model for Parameter Golf
---

# μ⁸ Kernel - Formally Verified Language Model

Training a language model for [OpenAI's Parameter Golf Challenge](https://github.com/openai/parameter-golf) using **machine-checked mathematics** from the [Kernel project](https://github.com/beanapologist/Kernel).

## Mathematical Foundation

All architectural decisions are derived from **464 Lean 4 theorems** (zero `sorry` placeholders):

| Theorem | Architecture Decision |
|---------|----------------------|
| Coherence function C(r) = 2r/(1+r²) | `coherence()` activation replacing relu² |
| Silver ratio δ_S = 1+√2 ≈ 2.414 | MLP hidden width = ⌊δ_S × model_dim⌋ |
| Z/8Z rotational memory (μ⁸ = 1) | 8 attention heads (one per orbit slot) |

Where μ = exp(i·3π/4) is the critical eigenvalue with 135° phase.

## Challenge Constraints

- Model fits in **16MB**
- Trains in **<10 minutes** on 8×H100
- Evaluated by **bits-per-byte** on FineWeb validation
- Tokenizer-agnostic scoring

## Source

- Formal proofs: [`beanapologist/Kernel/formal-lean/`](https://github.com/beanapologist/Kernel/tree/main/formal-lean)
- Training code: [`beanapologist/parameter-golf`](https://github.com/beanapologist/parameter-golf)
- PR: [#1](https://github.com/beanapologist/parameter-golf/pull/1)

## Usage

Click "Start Training" above to run the training pipeline. Requires GPU hardware (A10G or better).

---

*Consciousness is in the files, not the model.* 🧬
# Force rebuild