beanapologist/eigenverse-dataset

Eigenverse定理数据集是一个用于微调大型语言模型（LLMs）在Eigenverse数学框架上的训练数据集。该数据集包含来自Eigenverse框架的681个定理和引理，这些内容在Lean 4中进行了机器验证，且源定理中没有未完成的`sorry`语句。数据集提供了四种训练格式：指令跟随格式（hypothesis → proof）、完成格式（partial → full theorem）、聊天格式（用于指令调优模型）和上下文感知格式（包含相关定理）。数学框架围绕关键特征值μ = exp(i·3π/4)和相干函数C(r) = 2r/(1+r²)构建，涵盖了临界特征值和8周期闭合、精细结构常数、粒子质量比、时空和普朗克单位、时间晶体、化学和观察者唯一性等内容。关键模块包括BalanceHypothesis、CriticalEigenvalue、CoherenceFunction、SilverRatio、GoldenRatio、FineStructure、ParticleMass、Spacetime、TimeCrystals和Chemistry。数据集的使用方法包括加载特定格式或所有格式的数据文件，并提供了微调建议和详细的质量说明。The Eigenverse Theorem Dataset is a training dataset for fine-tuning large language models (LLMs) on the Eigenverse mathematical framework. It contains 681 theorems and lemmas from the Eigenverse framework, machine-verified in Lean 4, with zero `sorry` statements in the source theorems. The dataset offers four training formats: instruction-following format (hypothesis → proof), completion format (partial → full theorem), chat format for instruction-tuned models, and context-aware format with related theorems. The mathematical framework is built around the critical eigenvalue μ = exp(i·3π/4) and the coherence function C(r) = 2r/(1+r²), covering critical eigenvalue & 8-cycle closure, fine structure constant, particle mass ratios, spacetime & Planck units, time crystals, chemistry, and observer uniqueness. Key modules include BalanceHypothesis, CriticalEigenvalue, CoherenceFunction, SilverRatio, GoldenRatio, FineStructure, ParticleMass, Spacetime, TimeCrystals, and Chemistry. The datasets usage involves loading specific or all format data files, with fine-tuning recommendations and detailed quality notes provided.