README.md

metadata

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 using machine-checked mathematics from the Kernel project.

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/
• Training code: beanapologist/parameter-golf
• PR: #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