Repository navigation
Formalization Scope
Theorem Library formalizes claims that can materially narrow the research space.
A result belongs here when a machine-checkable proof can:
- settle a mathematical property that would otherwise motivate unnecessary experiments;
- expose a hidden assumption;
- rule out a proposed mechanism as stated;
- distinguish a local operator fact from a global/recurrent claim;
- create a reusable formal checkpoint for multiple research notes.
Empirical measurements, model-training results, literature summaries, active hypothesis queues, and private theorem-ledger lifecycle state are not public-library content simply because mathematics is involved.
A recurring failure mode is promoting a true local theorem into a stronger systems claim.
For example, the exact derivative of normalization is a local mathematical fact. A multi-layer or recurrent network may mix directions before or after that normalization. The formal library therefore includes composition boundaries rather than assuming the local result automatically propagates through the system.
The formal theorem and the empirical claim remain separate artifacts. Research Notes documents why a theorem matters to an experiment and what stronger interpretation does not follow.