Formalizing structures and trusted kernels

A small monoid can be represented by a small set-level carrier, a binary operation on it, a chosen unit, and proofs of associativity and the two unit laws. The operations are data, while the law fields assert identities for every tuple of carrier elements. In a setting with function extensionality, these law fields are mere propositions when the carrier is a set. This does not make the entire structure a mere proposition: different carriers or operation tables remain genuine alternatives.

Universe levels follow the carrier field and its packaging. Quantifying over all small monoids generally belongs in a larger universe than a single small carrier. One must also distinguish a chosen structure from a mere assertion that such a structure exists. The latter may be propositionally truncated and cannot automatically supply an operation table. Names such as group or ring are not enough: the signature and laws must be checked for omitted conditions, including whether an inverse is data or merely asserted to exist.

Given an equivalence between carriers, define the new unit by mapping the old unit, and define the new operation by moving both arguments back, using the old operation, then mapping the result forward. Inverse laws supply the identities needed to transport associativity and the unit equations. A bare equivalence does not usually preserve an unchanged operation table. The operation must be transported or a separate homomorphism property must be proved.

In a univalent foundation, appropriate structure-identity principles relate equivalences preserving structure to equalities of the corresponding packaged structures. Their hypotheses concern the specified signature and laws; univalence of carriers alone does not bypass the operation obligations. A conventional proof assistant with a different equality theory may instead use explicit isomorphisms and rewriting lemmas. Both styles can formalize the same algebraic calculation while relying on different foundational rules and offering different judgmental computations.

Lean's official reference describes a small kernel that checks elaborated core terms and new declarations. The elaborator resolves notation, implicit arguments, and tactics before that check; ordinary tactic success must still produce an acceptable term. The kernel does not itself run the surface termination checker or general unification search. Recursive definitions are elaborated into accepted recursors. These implementation facts concern Lean's specified core theory, whose proof-irrelevant Prop is not identical to the proof-relevant intensional theory used throughout the preceding examples.

An axiom is a declared constant, not a theorem whose consistency the kernel proves. Lean tracks proof dependencies so an axiom audit can reveal classical choice, other foundational assumptions, and unfinished-proof placeholders. The reference also distinguishes native-evaluation proofs that expand the trusted computational base. A checked result is therefore relative to its environment, checking implementation and relevant execution assumptions. It still requires human scrutiny that its formal statement matches the intended mathematical problem; a perfectly checked theorem about the wrong operation proves the wrong claim.