A Dictionary Whose Definitions Compile

Every dictionary you have ever used is circular. Open one and chase a word downward: "woman" points to "adult" and "human", "adult" points to "mature", "mature" points to "fully developed", "developed" points back, eventually, to something you started with. Lexicographers know this and shrug; a dictionary is a device for people who already speak the language, so the circle is load-bearing. It works for us because we bring the meanings with us.

But suppose you wanted a dictionary that did not assume the reader already knows everything. A dictionary where every definition is built strictly from more fundamental pieces, where circularity is not merely discouraged but impossible, where the claim "this word means exactly this" is checked by a machine rather than asserted by an editor. I have started building one, in Lean 4, and this essay is the report: what is possible, what is impossible in principle, what the first compiling fragment looks like, and why the famous word-vector arithmetic (the one where hitler − germany + italy ≈ mussolini) turns out to be a lossy shadow of something a proof assistant can state exactly.

Everything below marked as Lean is real code. It compiles, today, on Lean 4.29.1, with zero unproven claims. Where I show a theorem, a kernel has checked it.

1. An old dream with a new substrate

The idea is not new. Leibniz wanted an alphabetum cogitationum humanarum, an alphabet of human thoughts from which every concept could be composed. John Wilkins published An Essay towards a Real Character and a Philosophical Language in 1668, a full taxonomy of meaning with a synthetic vocabulary hung off it. Modern lexicography made the circle explicit and managed it: the Longman dictionary defines all its entries using a controlled defining vocabulary of roughly two thousand words (which are, of course, circular among themselves). WordNet organised the lexicon as a graph of typed relations. The Cyc project spent decades hand-coding common sense in logic. And Anna Wierzbicka's Natural Semantic Metalanguage programme made the strongest empirical claim of all: that around sixty-five semantic primes (I, you, want, know, good, big, do, happen, and their kin) occur in every human language and suffice to define everything else without circularity.

What none of these had was a kernel: an independent, tiny, incorruptible checker that refuses to accept a circular definition, refuses a dangling reference, and can verify, mechanically, that a claimed consequence of a definition actually follows. Proof assistants have exactly that. Lean's kernel will not elaborate a definition that refers to itself or to anything not yet defined. The very property lexicographers gave up on is the default behaviour of the tool.

There is a pleasing inversion here. In a paper dictionary, non-circularity is an unattainable ideal. In Lean, it is not even a discipline you must maintain; it is structurally impossible to violate. The question stops being "how do we avoid circles?" and becomes "what do we ground out in?"

2. The trilemma, resolved by honesty

Chase definitions downward and only three things can happen: you loop (circularity), you never stop (infinite regress), or you hit ground (undefined primitives). Philosophers call this the Münchhausen trilemma, and no definitional system escapes it. Banning the first two forces the third: every non-circular dictionary must declare a primitive basis, a set of concepts it refuses to define.

This is not a defect to hide; it is the most honest line in the whole project. Lean itself grounds out in a handful of primitives (dependent function types, inductive types, universes). Mathematics grounds out in axioms. My pilot dictionary grounds out, for now, in six declared primitives: entity, parent-of, female, male, human, adult. Each carries a note saying why it is bedrock this round and what a deeper decomposition would look like (the biological layer waits below "female"; the jurisdiction-relative thresholds of law wait below "adult").

Lean gives you something delightful on top: #print axioms reports, for any definition, the complete set of primitives it ultimately rests on. Every word in this dictionary has a machine-derivable grounding trace. Ask what "cousin" rests on and the answer is not an editor's opinion; it is a computation.

3. Genus and differentia, kernel-checked

The classical theory of definition, from Aristotle by way of the medieval logicians, says a definition names a genus (the broader kind) and differentiae (what distinguishes this from the rest of the kind). It is the natural shape for a compositional dictionary, and for a satisfying fragment of the lexicon it simply works. Here is the pilot's object language. The definitions are parametric over a World, any domain of entities equipped with the primitive predicates, so nothing about the actual world is asserted; what is asserted is how the words relate:

structure World where
  Entity : Type
  parentOf : Entity → Entity → Prop
  female : Entity → Prop
  male : Entity → Prop
  human : Entity → Prop
  adult : Entity → Prop

variable (W : World)

/-- woman := human ∧ female ∧ adult (genus: human; differentiae: female, adult). -/
def Woman (x : W.Entity) : Prop := W.human x ∧ W.female x ∧ W.adult x

def Girl (x : W.Entity) : Prop := W.human x ∧ W.female x ∧ ¬ W.adult x

def Mother (p c : W.Entity) : Prop := W.parentOf p c ∧ W.female p

/-- Siblinghood: distinct entities sharing a parent. -/
def Sibling (x y : W.Entity) : Prop :=
  x ≠ y ∧ ∃ p, W.parentOf p x ∧ W.parentOf p y

/-- Grandparenthood is parenthood composed with itself. -/
def Grandparent (g c : W.Entity) : Prop :=
  ∃ p, W.parentOf g p ∧ W.parentOf p c

And now the part no paper dictionary can do. The taxonomy is not asserted; it is proved, and the proofs are one line each because they fall straight out of the definitions:

theorem woman_human (x : W.Entity) : Woman W x → W.human x := fun h => h.1

/-- Girls are not women: the differentia `adult` separates them. -/
theorem girl_not_woman (x : W.Entity) : Girl W x → ¬ Woman W x :=
  fun hg hw => hg.2.2 hw.2.2

/-- Siblinghood is symmetric — provable from the definition alone. -/
theorem sibling_symm (x y : W.Entity) : Sibling W x y → Sibling W y x :=
  fun ⟨hne, p, hx, hy⟩ => ⟨fun h => hne h.symm, p, hy, hx⟩

/-- A mother's mother is a grandparent. -/
theorem mother_mother_grandparent (g p c : W.Entity) :
    Mother W g p → Mother W p c → Grandparent W g c :=
  fun hg hp => ⟨p, hg.1, hp.1⟩

Read the second theorem again. "Every girl is not a woman" is the kind of sentence a dictionary implies but never checks. Here it is a one-line proof: a girl's non-adulthood contradicts a woman's adulthood. If someone later edits the definition of girl in a way that breaks this, the dictionary stops compiling. Semantic drift becomes a build error.

4. Where the classical theory fails, grade it, do not fake it

If genus and differentia worked everywhere, philosophy would have finished this project centuries ago. It does not work everywhere, and the failures are famous. Wittgenstein challenged anyone to state necessary and sufficient conditions for game; the concept holds together by family resemblance, not by a boundary. Eleanor Rosch showed experimentally that category membership is graded: a robin is a better bird than a penguin. Decades of conceptual analysis died on words like knowledge and cause.

A dictionary that pretends otherwise is lying, and lying is the one thing this project exists to make impossible. So the definitional strength of every entry is a constructor, not a hope:

inductive DefKind
  | iff        -- full definition: the Lean anchor is necessary AND sufficient
  | necessary  -- the anchor states only necessary conditions (honest partial)
  | sufficient -- the anchor states only sufficient conditions (honest partial)
  | prototype  -- family-resemblance concept: no sharp boundary exists
  | primitive  -- declared bedrock: undefined BY DESIGN

A necessary-only entry is not a failure; it is a machine-checked partial truth, which is strictly more than a prose dictionary gives you. Poka-yoke (the Japanese manufacturing term for mistake-proofing design) sits in the pilot as a prototype: I can gesture at it, I can give examples, and the entry honestly records that no sharp boundary has been formalised. The pilot's census is computed, not estimated: of twenty-one entries, thirteen are formal, two are prototypes, six are declared primitives. A well-formedness suite runs over the whole structure and is proved by the kernel:

theorem dict_wellFormed : wellFormed dict = true := by decide

where wellFormed conjoins: every concept has exactly one entry, every cross-reference resolves, every formal entry actually carries a Lean anchor (a formal claim without a kernel object behind it is theatre, and the checker rejects it), every entry has at least one word-form, and the reference graph is acyclic. The suite also catches violations, verified negatively: a chicken-and-egg dictionary fails acyclic, and an entry claiming iff with no anchor fails anchorsHonest. Both rejections are themselves theorems.

One honesty note the project's own standards demand. These proofs originally used native_decide, which trusts Lean's compiled evaluator in addition to the kernel proper. They have since been migrated to plain decide, so the kernel alone checks them: #print axioms now reports that dict_wellFormed depends on no axioms whatsoever, and the no-contamination theorem below depends only on propext. The distinction is worth stating in an essay about not overclaiming, and worth closing rather than merely noting.

5. Contested words: split the senses, do not adjudicate them

The alert reader noticed I defined woman and will have views. Here is what formalisation actually does with contested words, and I think it is the most socially useful property of the whole approach: it forces sense-splitting. The pilot's entry is explicitly the sex-referring sense, and its gloss says so: the gender-referring sense is a distinct entry with a distinct definition, to be added in a later round. One signifier, two signifieds, two entries.

David Chalmers has argued that a large fraction of philosophical (and, one might add, political) disputes are verbal: the parties share the facts and differ over which meaning a word should carry. A dictionary in which every sense is a separate, precisely defined object cannot host a verbal dispute. You can still disagree about which sense a law or a policy should invoke, and that disagreement is real and normative. But "what does the word mean?" stops being the battlefield, because the answer is: it means each of these things, precisely, pick the one you are arguing about. The formal move is neutral by construction; it adjudicates nothing and clarifies everything.

6. One signified, many signifiers

A dictionary is not an ontology. An ontology has concepts; a dictionary binds words to concepts, and the binding deserves first-class structure. Following the linguists: a sign pairs a signifier (the word-form) with a signified (the concept). In the pilot, every entry carries a list of signifiers, each tagged with language and, where measured, its cost in model tokens:

structure Signifier where
  lang : String            -- en / es / fr / it / la / de / ja / coined
  form : String
  tokenCost : Option Nat := none      -- per model tokeniser; none = unmeasured
  pretrainedChecked : Bool := false   -- zero-context comprehension check passed

So woman carries mujer, femme, donna alongside the English; sibling carries the German Geschwister, which bundles the brother-and-sister collective into a single word; poka-yoke is carried in Japanese because that is where the precise word lives. This is a deliberate strategy, not decoration: when you need a handle for a concept, a word that already exists in some language is enormously cheaper than a coinage, because every competent speaker (human or model) already carries its meaning. Only where no language has the word do you coin one, and then the Lean definition is the coinage's anchor: the meaning is fixed by the kernel before the word has any usage history at all. A brand-new word with a machine-checked meaning is a strange and rather wonderful object; it inverts the usual order in which usage comes first and dictionaries catch up.

The polysemy machinery falls out of the same structure. Synonymy is two signifiers sharing a signified. Ambiguity is one signifier mapping to several signifieds, and it is detectable by a query rather than by vigilance. My working rule that a good technical term needs high sensitivity and high specificity, with carve-outs as evidence of failure, becomes partially mechanical: a specificity failure is literally a signifier resolving to more than one in-scope entry.

7. The vector layer: what hitler − germany + italy is really doing

Now the second half of the story. Word embeddings, made famous by Mikolov and colleagues in 2013, revealed that models trained on co-occurrence statistics arrange words in a space where certain analogies become arithmetic: king − man + woman lands near queen; capital cities line up with their countries along a consistent direction. My own favourite instance of the pattern: hitler − germany + italy should land near mussolini. When I reach for an analogy in conversation (and friends tell me analogies are the thing my brain does), I am fairly sure something like this is happening: subtract the context, carry the relational structure, add the new context, read off the answer.

Here is the reframe the formal side makes available. Ask what makes the mussolini analogy true. It is not a fact about vectors; it is a fact about a relation: "leader of, in 1938" maps Germany to Hitler and Italy to Mussolini. The parallelogram in embedding space is a lossy statistical shadow of that typed relation. The exact content is small, sharp, and checkable:

def facts : List Edge := [
  { rel := "leaderOf@1938", src := "germany", dst := "hitler",
    note := "head of government, Germany, 1938" },
  { rel := "leaderOf@1938", src := "italy", dst := "mussolini",
    note := "head of government, Italy, 1938" },
  { rel := "capitalOf", src := "germany", dst := "berlin" },
  { rel := "capitalOf", src := "france", dst := "paris" },
  { rel := "capitalOf", src := "italy", dst := "rome" },
  { rel := "capitalOf", src := "japan", dst := "tokyo" }
]

The vector version is fragile in ways the literature has documented (the reported analogy accuracies depended, among other things, on excluding the input words from the candidate answers). So the dictionary carries vector-style conjectures as data about a model's geometry, tagged with the weakest evidence grade in the system:

inductive SemEvidence | proved | distributional

distributional is the formal name for the flag I wanted: a "rough semantic vectorial guideline" that lives in the system as a constructor, not a comment, and the machinery treats it accordingly.

8. The wall, as a theorem

The danger with keeping rough guidelines next to proved facts is contamination: a plausible conjecture quietly becomes a premise, three steps later it is load-bearing, and the system's outputs inherit the noise. The classic fix is organisational (keep them in different files, hope everyone behaves). The fix here is a theorem.

Derivation in the dictionary (composing relations: leader-of composed with capital-of, and so on) is defined to consume only proved edges. Then the pilot proves, by kernel computation over the actual data:

/-- Adding the entire distributional shadow to the knowledge base
    changes NOTHING derivable. -/
theorem no_contamination : derivable (facts ++ shadow) = derivable facts := by
  decide

The vector layer may suggest; it can never assert. This mirrors a design my broader world-modelling stack already uses (a grade lattice with a proved no-uplift rule: no fact's epistemic grade can silently rise). Different codebase, same moral: honesty is cheap to state in prose and worthless there; state it where a kernel can hold it.

9. The loop: geometry proposes, the kernel disposes

Once the wall exists, the two layers stop being rivals and become a pipeline. Embedding geometry is a conjecture generator: cheap, wide, noisy, occasionally inspired. The relational layer is a verifier: exact, narrow, incorruptible. A conjecture is promoted only when a single proved relation explains both pairs:

def Analogy.verified (an : Analogy) (es : List Edge) : Bool :=
  (provedEdges es).any fun e1 =>
    e1.src == an.b && e1.dst == an.a &&
      (provedEdges es).any fun e2 =>
        e2.rel == e1.rel && e2.src == an.c && e2.dst == an.d

theorem mussolini_promoted : conj_mussolini.verified facts = true := by decide
theorem rome_promoted : conj_rome.verified facts = true := by decide

And, just as importantly, the verifier rejects. A conjecture the geometry might plausibly emit, hitler − germany + france ≈ napoleon, is wrong by a century, and the system says so as a theorem:

theorem napoleon_rejected : conj_napoleon.verified facts = false := by decide

The compositional wing of this idea has serious prior art: Montague showed in the 1970s that natural-language meanings can be typed lambda terms (a Lean dictionary is, in that sense, executable Montague semantics), and the DisCoCat programme of Coecke, Sadrzadeh and Clark unified distributional vectors with compositional grammar in monoidal categories. What I have not seen built is the humble engineering complement: machine-checked distributional semantics with promotion rules. Point the generator at a real embedding table (a named model, a recorded snapshot), let it emit thousands of parallelogram conjectures, and let the verifier sort them into promoted, rejected, and undecided-pending-more-edges. The promoted set is mined knowledge with proofs; the rejected set is a map of exactly where the model's geometry lies about the world; the ratio between them is an honesty metric for the embedding space itself. That is the next milestone on this project's roadmap.

10. Why bother: humans, machines, and the analogy engine

Three reasons this is worth the candle beyond the intellectual fun.

For thinking. If good analogies are relational algebra (strip the context, keep the relation, rebind the context), then a dictionary of typed relations is an analogy engine you can trust: it will tell you which of your parallelograms are load-bearing and which are just pretty. The difference between a good analogy and a misleading one is precisely whether a single relation really does map both pairs, and that is now a decidable question.

For words that matter. Contested definitions run through law, policy, medicine, and family life. Sense-splitting with kernel-anchored definitions will not settle normative arguments (nor should it), but it removes the ambiguity that lets verbal disputes masquerade as substantive ones. A contract, a statute, or a diagnostic criterion whose defined terms have grounding traces is a different kind of document.

For machines. Recent interpretability work suggests language models maintain a small, capacity-limited workspace of verbalisable concepts, indexed by tokens. If that picture holds, then which words exist, and how precisely they are anchored, is not just a communication question; it shapes what a model can hold in mind and manipulate. (This complements interpretability research rather than replacing it: reading a model's internals and improving the vocabulary those internals are indexed by are different layers of the same defence.) A dictionary whose definitions compile is the strongest anchoring signal one can publish: a term co-occurring, in public text, with a machine-checked definition is about as clean a training example as the next generation of models will ever see. This essay is, deliberately, the first such seed for the entries above.

11. The strongest objections, taken seriously

"Your theorems are trivial: you only proved projections of your own definitions." Correct, and that is the point at this stage. woman_human is a one-line projection because the definition was built compositionally; the theorem's value is not its difficulty but its permanence: any future edit that breaks the taxonomy breaks the build. The non-trivial theorems (symmetry of siblinghood and cousinhood, the no-contamination result, the promotion and rejection verdicts) are small but genuine, and the negative tests prove the checkers can actually fail. A dictionary does not need deep theorems; it needs an immune system.

"Cyc spent decades and hundreds of person-years on this and did not conquer common sense. Twenty-one entries will not either." Also correct, and the census is printed rather than hidden precisely so nobody mistakes a pilot for a lexicon. Two things have changed since Cyc started, though. Proof kernels replaced bespoke inference engines, so the checking substrate is now commodity-grade and trustworthy. And large language models inverted the economics: the expensive part (broad coverage of meaning) now exists statistically in every model, so the scarce artefact is no longer coverage but anchoring, exact fixed points the statistical mass can be checked against. A small dictionary of anchors plus a generator/verifier loop is a different bet from hand-coding everything.

"Pinning words down destroys ambiguity, and ambiguity is load-bearing." In diplomacy, poetry, and early-stage design, deliberately unresolved meaning does real work, and a formalisation that paved over it would be a loss. The graded entry kinds are the answer within the system: a prototype entry is the formal acknowledgement that a sharp boundary does not exist (and would be a lie). The dictionary's ambition is not to eliminate ambiguity but to make it a recorded, chosen property of an entry rather than an accident nobody noticed.

"Formally defining words like 'woman' is politically naive; the definition smuggles in a position." The system's answer is sense-splitting (section 5): each sense is a separate object, precisely stated, and choosing between senses for a given purpose remains a human, normative act that no kernel can or should perform. What the formalisation removes is only the ability to run the two senses together and call the confusion an argument. If anything, the discipline forces the normative question into the open, which is where it belongs.

12. What exists, honestly stated

As of today: a two-file, dependency-free Lean 4 library. One file is the engine (definition kinds, signifiers, entries, decidable well-formedness, typed edges, analogy conjectures, the verifier). One file is the pilot (the kinship object language with its theorems, twenty-one dictionary entries across four definition grades and eight language tags, the relational facts, the distributional shadow, the no-contamination theorem, and the promotion and rejection theorems). Since first publication it has also grown machine-derivable grounding traces (primitiveBasis dict "cousin" returns exactly ["parent-of", "entity"]), a theorem that every formal entry grounds out in the declared primitives, its converse that the ungrounded entries are exactly the prototypes the dictionary admits it has not defined, and polysemy detection, which reports that the pilot binds no word-form to two meanings while catching the bank case that does. It builds in about a second. There are no unproven claims in it; where honesty required weakness, the weakness is a constructor.

What it is not, yet: big. Twenty-one entries is a proof of shape, not a lexicon. The known-impossible parts (primitive bases, prototype concepts) are declared, not solved, because they are not solvable, and the entries say so. The obvious next rounds: decompose the current primitives one layer further and compare the basis against Wierzbicka's primes; wire the entries into the stratified world-model this project sits beside; and build the embedding-mining loop against a real model's vectors.

The deeper ambition is slower and stranger: to grow a vocabulary, some borrowed from the languages that already have the right words, some coined, each anchored to a definition a kernel checks, published where both people and future models will read it, and to watch which of those words the world decides to keep.

Written with my AI research partner in a single day's session; the Lean code was written, compiled, and kernel-checked before a word of this essay was drafted. Every code block above is verbatim from the repository and compiles as shown. The pilot currently lives in my private monorepo; a public extract is planned once the entry format stabilises. Lean 4.29.1; thirty-three theorems; zero sorry; proofs checked by the kernel alone.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.