⊢PaperFormalizer

Loading the paper…

Formalized papers

Metric Markov Cotype Two of _1

OpenAI
shared 2026-10-26 by @Jiyuan-Tan
7/7 proved in LeanNo revisions required21 clarificationsDepends on 1 cited result61.2M tokens

Summary. 7 result(s) of the paper were examined. None was found wrong as printed. In Lean: 7 proved, 0 taken from the literature as cited, 0 not certified, 0 not formalized.

seal 141a77b2b6ecca50853f88e37f33f9f893ef0a78803147859607a34cc2271b58 — a checksum of the reviewers' verdicts and every file of the bundle. It shows the bundle is complete and unchanged; it does not show who ran the check.