Epiplexity
Machine-checked Lean 4 formalization of Finzi et al.'s Epiplexity framework. Time-bounded complexity via MDL decomposition: S_T(X) measures code length (structure), H_T(X) measures cross-entropy (noise). CSPRNG indistinguishability implies high epiplexity. One-way permutation implies factorization hardness. 23 modules, 0 sorry.
Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
Epiplexity • Lean 4 + Mathlib • Apoth3osis Labs
Key Mathematics
MDL Decomposition
Lean: OptimalProg.MDLT, MDLT_eq_mdlCost
CSPRNG → High Epiplexity
Lean: csprng_high_epiplexity via PRFHighEpiplexity
OWP Factorization Hardness
Lean: owp_factorization_hardness
Paper ↔ Proof Correspondence
| Claim | Theorem | Status |
|---|---|---|
| MDL decomposition: MDL_T = S_T + H_T | MDLT_eq_mdlCost | ✓ |
| Epiplexity is nonneg | ST_nonneg | ✓ |
| Cross-entropy is nonneg | HT_nonneg | ✓ |
| CSPRNG implies high epiplexity | csprng_high_epiplexity | ✓ |
| OWP implies factorization hardness | owp_factorization_hardness | ✓ |
| Optimal program is MDL-minimal | OptimalProg.optimal | ✓ |
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.