How the computer learns a new meaning.

Design notes about proof-native programs, games, markets, and the machinery beneath them. The theorem-by-theorem ledger lives at the technical twin.