beanapologist/eigenverse-dataset

---
language:
- en
license: mit
task_categories:
- text-generation
tags:
- lean4
- theorem-proving
- eigenverse
- mathematics
- physics
pretty_name: Eigenverse Theorem Dataset
size_categories:
- 1K<n<10K
configs:
- config_name: chat
data_files: eigenverse_chat.jsonl
- config_name: instruct
data_files: eigenverse_instruct.jsonl
- config_name: completion
data_files: eigenverse_completion.jsonl
- config_name: context
data_files: eigenverse_context.jsonl
---

# Eigenverse Theorem Dataset

Training data for fine-tuning LLMs on the Eigenverse mathematical framework.

## Dataset Description

681 theorems and lemmas from the [Eigenverse framework](https://github.com/beanapologist/Eigenverse), machine-verified in Lean 4. Zero `sorry` statements in the source theorems.

The dataset contains four training formats:
- **`eigenverse_instruct.jsonl`** (681 examples) — instruction-following format (hypothesis → proof)
- **`eigenverse_completion.jsonl`** (681 examples) — completion format (partial → full theorem)
- **`eigenverse_chat.jsonl`** (681 examples) — chat format for instruction-tuned models
- **`eigenverse_context.jsonl`** (681 examples) — context-aware format with related theorems

## Mathematical Framework

Built around **μ = exp(i·3π/4)**, the critical eigenvalue, and coherence function **C(r) = 2r/(1+r²)**.

The framework covers:
- **Critical eigenvalue & 8-cycle closure** (μ⁸ = 1)
- **Fine structure constant** (α ≈ 1/137 from μ¹³⁷ = μ)
- **Particle mass ratios** (electron/muon/tau via golden & silver ratios)
- **Spacetime & Planck units** (dimensional analysis)
- **Time crystals** (temporal coherence)
- **Chemistry** (NIST atomic weights, periodic table structure)
- **Observer uniqueness** (`reality_unique` - any balanced observer must equal μ)

### Key Modules

- `BalanceHypothesis` - Core balance theorems (|Re(μ)| = Im(μ) = η = 1/√2)
- `CriticalEigenvalue` - 8-cycle properties, phase geometry
- `CoherenceFunction` - C(r) properties, kernel/silver/golden scales
- `SilverRatio` - δ_S = 1 + √2 ≈ 2.414, C(δ_S) = √2/2
- `GoldenRatio` - φ relationships, Koide formula
- `FineStructure` - α derivation, μ¹³⁷ = μ proof
- `ParticleMass` - Lepton mass predictions
- `Spacetime` - Dimensional coherence
- `TimeCrystals` - Temporal oscillation modes
- `Chemistry` - Atomic weight predictions

## Data Format Examples

### Chat Format (eigenverse_chat.jsonl)

```json
{
"messages": [
{
"role": "system",
"content": "You are a Lean 4 theorem proving assistant for the Eigenverse framework..."
},
{
"role": "user",
"content": "Formalize this hypothesis in Lean 4: The real part of the critical eigenvalue equals the negative of the canonical balance constant."
},
{
"role": "assistant",
"content": "```lean4\n-- BalanceHypothesis\ntheorem mu_re_is_neg_eta : μ.re = -η := by\n sorry\n```"
}
]
}
```

### Context-Aware Format (eigenverse_context.jsonl)

```json
{
"messages": [
{
"role": "system",
"content": "You are an Eigenverse theorem proving assistant."
},
{
"role": "user",
"content": "Given these existing theorems:\nmu_im_is_eta: μ.im = η\neta_pos: 0 < η\n\nProve: The real part of the critical eigenvalue equals..."
},
{
"role": "assistant",
"content": "```lean4\ntheorem mu_re_is_neg_eta : μ.re = -η := by\n have h1 := mu_im_is_eta\n have h2 := eta_pos\n sorry\n```"
}
]
}
```

## Usage

```python
from datasets import load_dataset

# Load chat format
ds = load_dataset("beanapologist/eigenverse-dataset", data_files="eigenverse_chat.jsonl")

# Or load all formats
ds_all = load_dataset("beanapologist/eigenverse-dataset", data_files="*.jsonl")
```

## Fine-Tuning Recommendations

- **Base model:** TinyLlama-1.1B-Chat-v1.0 or similar small instruction-tuned LLM
- **Method:** LoRA (rank=16, alpha=32)
- **Learning rate:** 2e-4
- **Epochs:** 3-5
- **Batch size:** 4-8 (depending on GPU)

See `finetune_config.md` in the repository for detailed instructions.

## Quality Notes

Natural language descriptions are extracted from theorem docstrings in the original Lean 4 codebase, providing precise mathematical context directly from the formalization.

## Source

- **Repository:** https://github.com/beanapologist/Eigenverse
- **Theorems:** 552 fully proven (0 `sorry`), 681 theorem/lemma declarations in KB
- **Framework:** Lean 4 with Mathlib
- **License:** MIT

## Citation

If you use this dataset, please cite the Eigenverse framework:

```bibtex
@misc{eigenverse2026,
author = {beanapologist},
title = {Eigenverse: A Pre-Physical Framework from μ = exp(i·3π/4)},
year = {2026},
url = {https://github.com/beanapologist/Eigenverse}
}
```

## Related Work

- [Eigenverse Prover](https://github.com/beanapologist/eigenverse-prover) - Automated theorem proving agent
- Fine-tuned model: `beanapologist/eigenverse-llm` (coming soon)