MIRADOR: A Typed, Versioned Intermediate Representation for Auditable Mathematical Knowledge and Discovery

MIRADOR (Mathematical Intermediate Representation for Auditable Discovery, Organization, and Reasoning) is a prover-independent intermediate representation whose reusable unit is a typed, versioned Mathematical Cell binding a canonical claim to its context, dependencies, transformations, artifacts, provenance, and epistemic state. Object type is orthogonal to epistemic state; claim identity is the canonical hash of a statement and its context, so assumptions and scope participate in identity; transformations and reduction edges are first-class auditable objects; and invalidation propagates deterministically over an append-only, hash-chained event log. The work includes an executable JSON Schema, a dependency-free Python reference implementation (28 deterministic tests), and a case study on Bang's affine plank problem reconstructing five documented failures of a real manual campaign. MIRADOR is the representational substrate of the companion Bourbaki Engine. This record archives the paper, the arXiv-ready source, and the full software artifact.