Lean-Ready English

Every sentence I write about a rule is read twice: once by a person, once by a machine that turns it into Lean. The person brings context and charity. The machine, today usually a language model, brings a guess. When the guess is right nobody notices. When it is wrong, the formal model is precise about the wrong thing, and precision makes the error look trustworthy.

This essay proposes a way to take the guess out of the loop for the sentences where it matters: a controlled form of English whose every accepted sentence has one declared meaning in Lean, and a library of the constructions that carry those meanings. I call the first Lean-ready English and the second LangLib, by analogy with Mathlib. A first slice of both exists and compiles. It also caught a mistake in one of my own earlier essays, which is the best argument I have for it.

Every code block below comes from the repository, which compiles on Lean 4.29.1 with no sorry. Each block says whether it is verbatim or abridged. Every theorem named as proved was checked by the kernel and depends only on Lean's three standard axioms.

1. The terms

A new project needs its words fixed before it needs anything else, so here they are.

• Lean-ready English. A controlled subset of English in which every accepted sentence maps to exactly one value of a typed intermediate representation. Sentences outside the subset are rejected with a reason. It is English-shaped, not English-complete.
• Semantic IR. The intermediate representation: a small typed tree that records what a sentence means. It is the authority. Both the English and the Lean are generated from it or checked against it; neither is maintained by hand alongside it.
• LangLib. The library of constructions, each with a grammar pattern, a typed meaning in the IR, a canonical English rendering, a lowering to Lean, and theorems about it. Where a dictionary defines words, LangLib defines the patterns words are put into.
• Lexical entry versus construction. A lexical entry says what a word denotes ("processor" means a data processor). A construction says how denotations combine ("X holds only if Y holds" means X implies Y). The dictionary in A Dictionary Whose Definitions Compile supplies the first kind; LangLib adds the second.
• Canonical English. The one rendering of an IR value that LangLib produces. Several wordings may parse to the same IR; only one is printed back. In the current slice that happens once: "No X holds." and "X never holds." are the same rule, and only the second is printed.
• Round-trip fidelity. Rendering an IR value and parsing the result gives back the same value. This is the property that makes the English a faithful view of the formal object rather than a paraphrase of it.
• Rejected. The parser's answer to a sentence it cannot give a declared meaning. A rejection names the word or pattern at fault. It is the most important output the system has.
• Oracle verdicts. When two formalisations are compared, there are four outcomes, not two: Equivalent (with a proof), NonEquivalent (with a counterexample or proof), Unresolved (no proof either way yet) and Rejected (the input never reached a formal meaning). Failing to find an equivalence proof is Unresolved, not evidence of difference.
• Formalisation boundary. The declared point where formal determination stops: a term such as "reasonable care" is represented as an open-textured standard that needs a named determination, not quietly given a crisp definition.

2. The precedent is older than computing

The mechanics-manual analogy is exact. In the late 1970s European airlines asked their manufacturers' association, AECMA, to make the English in aircraft maintenance documentation harder to misread. The result became ASD-STE100, Simplified Technical English, now at Issue 9 (January 2025) and maintained by ASD's Simplified Technical English Maintenance Group. It restricts vocabulary and sentence patterns so that a technician with limited English reads one meaning.

Three later projects pushed the idea from "easy to understand" to "has a formal meaning". Attempto Controlled English, from Norbert Fuchs and Rolf Schwitter at the University of Zurich, translates its subset of English into discourse representation structures, a form of first-order logic. Aarne Ranta's Grammatical Framework separates a language-independent abstract syntax from language-specific concrete syntaxes, so the same tree can be parsed from text and rendered back into it, in several languages. Naproche, started at the University of Bonn by Bernhard Schröder and Peter Koepke, checks mathematical texts written in its controlled language ForTheL, and there has been work translating ForTheL-style input into Lean.

So none of this is new in principle. What is new is the target and the economics: Lean as the semantic back end, a kernel that checks the library's own claims, and language models cheap enough to draft controlled sentences that the parser then accepts or refuses.

3. The first slice: five constructions

I started where my own writing had already gone wrong: conditions. The slice has five constructions, each with one declared meaning. The fifth, a prohibition, was added after the first four met real requirements (section 5). (Abridged: the source carries docstrings where this shows one-line comments.)

inductive IR where
  | sufficientCondition    (cond concl : Ident)   -- "Q holds if C holds."              C → Q
  | necessaryCondition     (cond concl : Ident)   -- "Q holds only if C holds."         Q → C
  | necessaryAndSufficient (cond concl : Ident)   -- "Q holds if and only if C holds."  Q ↔ C
  | permission             (authority subject cond : Ident)
                                                  -- "A may grant S if C holds."  C → Permitted A S
  | never                  (x : Ident)            -- "X never holds." (also "No X holds.")  ¬ X

The grades are not new either. The dictionary already distinguished definitions that are full (iff), necessary only, or sufficient only. LangLib reuses that exact type, so a rule's strength and a word's definitional strength are one concept, checked once. (Verbatim.)

def IR.defKind : IR → Option LeanLex.DefKind
  | .sufficientCondition .. => some .sufficient
  | .necessaryCondition .. => some .necessary
  | .necessaryAndSufficient .. => some .iff
  | .permission .. => none
  | .never .. => none

Permission and prohibition have no grade, on purpose. "The authority may grant the visa" confers a power: it says what the authority may do, not that the applicant qualifies, and the lowering to Lean keeps it in a separate predicate.

Names cannot be grammar words, and a short list of words has no definition in this environment at all: unless, not, promptly, reasonable, soon, appropriate. Bare not stays undefined even now that never exists, because its scope is the classic ambiguity ("all applicants did not qualify"). A sentence that uses one is rejected with that word named, rather than given a plausible reading.

Two theorems carry the slice. The first is round-trip fidelity, proved for every IR value, not tested on samples (verbatim, proof included):

theorem parse_render (a : IR) : parse (render a) = .ok a := by
  cases a <;> simp [render, parse, mkIdent_of_ok]

That proof is short because the grammar was designed to make it short: the patterns have different lengths or different fixed words, and a name can never be a grammar word, which the identifier type enforces. Round-trip fidelity is cheap when you build for it and very hard to retrofit, which is the argument for building for it. It holds for every IR value whose names are valid identifiers, and the type admits no others.

The second says that "if" and "only if" are different rules: whenever the two names differ there is a world where the necessary condition holds and the sufficient one fails. A third confirms that the two together are exactly the biconditional. Two more cover the prohibition: "No X holds." parses to the same meaning as "X never holds.", and a prohibition defeats any sufficient condition for the prohibited thing. All of them depend only on Lean's standard axioms (propext, Classical.choice, Quot.sound).

One limit a semanticist will spot at once: these are whole-sentence patterns, not a compositional grammar. "Q holds only if C holds" is matched as a template; nothing yet builds it from a meaning for "only" and a meaning for "if". That is fine for five constructions and will not scale to fifty. The route to scale is the one Grammatical Framework took: an abstract syntax of small typed pieces with rules that combine them, so that new constructions are compositions rather than new templates.

4. The correction

In The Legal Reasoning Wind Tunnel I proposed testing a legal formaliser with deliberately varied phrasings of one rule. The example was a visa requirement of at least 183 days' physical presence, and I wrote that the first five variants "should canonicalise to the same IR and produce provably equivalent Lean terms". Two of them do not.

1. "An applicant qualifies if they have been physically present for at least 183 days." This is a sufficient condition: presence is enough to qualify.
2. "The visa may be granted to an applicant who has been physically present for at least 183 days." This confers a power on the authority. It does not say the applicant qualifies, and it does not say the visa must be granted.
3. "An applicant does not qualify unless they have been physically present for at least 183 days." This is a necessary condition: no qualification without presence. It does not say presence is enough.

Variants four and five (the universal "every applicant who..." form and the verbalised threshold) are restatements of the first and do belong together. Variants two and three are different rules. They agree with the first only if the missing direction is stated separately, which the essay did not do.

LangLib makes this mechanical. Variant three as written is rejected, because not and unless have no definition; its Lean-ready restatement is "applicant_qualifies holds only if present_183_days holds", which parses as a necessary condition. The kernel then checks the rest. (Verbatim statements; the four decide proofs are shown, the two existence proofs are a few lines each in the repository.)

theorem v1_kind : (parse v1).kind = "sufficient" := by decide
theorem v2_kind : (parse v2).kind = "permission" := by decide
theorem v3_as_written_rejected : (parse v3asWritten).kind = "rejected" := by decide
theorem v3_kind : (parse v3).kind = "necessary" := by decide

theorem v1_ne_v3 : ∃ env : Env,
    lower env (.necessaryCondition present qualifies)
      ∧ ¬ lower env (.sufficientCondition present qualifies)

theorem v1_ne_v2 : ∃ env : Env,
    lower env (.sufficientCondition present qualifies)
      ∧ ¬ lower env (.permission minister visa present)

This matters beyond one example. A wind tunnel is only as good as its labels. If the benchmark says two sentences mean the same and they do not, a translator that correctly keeps them apart is scored as a failure. LangLib gives the benchmark trustworthy labels: the intended relationship between variants is generated from IR values, not asserted in prose.

Why reject unless instead of giving it the necessary-condition reading? Because in statutes it often does something else. "A person is liable unless they acted in good faith" usually sets up a default rule with an exception that the other side must establish, which is defeasible reasoning, not a plain implication. Catala, the language for statutory computation designed by Denis Merigoux, Nicolas Chataing and Jonathan Protzenko with Sarah Lawsky, makes exactly this kind of exception first-class through prioritised default logic. The slice does not claim exceptions cannot be formalised; Catala shows they can. It refuses to choose between the two readings silently, and the next construction to admit is an exception with default-logic semantics, so that the drafter states which reading is meant.

5. First use: real requirements

The other place where English and Lean drift apart is in requirements. In Verified Specification as Code I noted that matching a requirement's identifier to a predicate's name does not show they mean the same thing; today a person checks that by reading. I took three live requirements from my own estate and restated their acceptance criteria in Lean-ready English: an internal security component, an event listener that replaces a one-minute poll, and a drafts-first outreach process in which colleagues approve emails before anything is sent.

The first pass, with four constructions, rejected a prohibition criterion in the security component. Before building anything I counted: across 212 internal requirement files holding 11,792 acceptance criteria, a keyword scan found negation words (never, no, not, without) in about 16% of criteria, more than any other construction LangLib lacked; quantifiers (every, each, all) came next at about 11%. A keyword count is a rough guide, not a parse, but it was enough to pick the next construction. So the prohibition went in, with its theorems, and the criterion now parses.

Across the three requirements there are fourteen criterion sentences. Ten parse; four are rejected. A selection, quoted as the parser sees them (rejected sentences are the closest literal wording, since there is no Lean-ready form for them yet):

1. "No message_processed_twice holds." Parsed: prohibition, same meaning as the canonical "message_processed_twice never holds."
2. "polling_works holds if listener_down holds." Parsed: sufficient condition.
3. "p2_sends holds only if owner_recorded_yes holds." Parsed: necessary condition. (P2 is the agent that drafts the emails.) The prose was "nothing is ever sent without the owner's recorded yes", which reads like a prohibition and is in fact a necessary condition on sending.
4. "median_time_to_seen is under 10 s." Rejected: no construction for a measured threshold.
5. "each p2_draft is matched to sent_items." Rejected: no quantifier yet.
6. "after 5 sent_unchanged_drafts p2_asks_owner once." Rejected: no construction for counts over time.
7. "terminal_gates_model is updated." Rejected: no construction for a change of state.

The verdict lists are themselves theorems, so a change to the library that alters any of these readings breaks the build. The rejections are the useful part. They show which constructions come next (quantifiers, thresholds, counts over time, state change) and they stop anyone, person or model, from quietly inventing a meaning for those criteria in the meantime.

The restatements also expose something the prose hid. In the security component, three of the four original criteria are necessary conditions on completion, not definitions of it. Written as prose, "a spec exists" reads as if it finishes the job. Written as "done holds only if the spec exists", it plainly does not.

6. What a firm could do with it

The same move applies wherever a firm writes down a commitment it will later be held to: the acceptance criteria in a statement of work, the obligations schedule of a data processing agreement, the answers in a client's security questionnaire. Restate each commitment in Lean-ready English before it goes out, internally, and two things happen. Every sentence that parses has one meaning both sides can read back, so a condition such as "acceptance holds only if test_data_supplied holds" cannot later be argued into its converse, that supplying test data guarantees acceptance. Every sentence that is rejected is a commitment nobody can test yet, which is exactly the list a careful reviewer wants before signing. The client never sees the controlled form; the firm sees which of its promises it could prove it kept.

What this needs from a firm is modest: someone who owns the vocabulary for a document type, and a review step where canonical English is approved. What it does not yet have is the obligation and deadline constructions that most contract clauses need. That is the next slice, not this one.

7. Where the language model sits

The design keeps the model outside the boundary where meaning is decided. A model may draft Lean-ready sentences from loose prose, and it is good at that. The parser accepts or rejects them deterministically. A person approves the IR through its canonical English. The lowering to Lean is a function with theorems about it. Nothing the model says becomes a formal meaning without passing a check that does not depend on the model.

That is the same separation the dictionary made between proved facts and distributional suggestions, applied to sentences instead of words.

8. The strongest objections

"Nobody will write in a controlled language." Maintenance engineers have for forty years, because the cost of misreading was high enough. The same is true of acceptance criteria and contract obligations. And the authoring burden falls mostly on the drafting model; the person reads canonical English and approves.

"Five constructions is a toy." It is a first slice, chosen because it was where real errors were, and it already decides ten of fourteen real criteria. The next constructions follow from the rejections above and the keyword count: quantifiers, thresholds, counts over time and state change, then deadlines and obligations, each with its own theorems before it is admitted.

"People will write for the parser, not for the meaning." This is the Goodhart risk, and it is real. If the success measure is the share of sentences that parse, a drafting model will bend requirements into whatever pattern is accepted, and a necessary condition will become a sufficient one because the sufficient pattern was the one that parsed. The counter is the review step and the right metric: a person approves the canonical English, and the number worth tracking is how often a parsed sentence turns out to say something its author did not mean. Parse rate is a vanity number.

"Real legal language is open-textured, so this cannot reach it." Correct, and the system should say so. Lean-ready English does not mean every sentence becomes decidable. It means every accepted sentence has an explicit representation, including sentences that declare where formal determination stops.

9. What exists now

A small Lean 4 library, stdlib-only, that depends on the dictionary for its definition grades. It has five constructions, a deterministic parser with diagnostics, a canonical renderer, a lowering to Lean propositions, a general round-trip theorem, the non-equivalence, biconditional and prohibition theorems, the wind-tunnel correction and three real requirements restated (fourteen criteria, ten parsed, four rejected). It does not yet have quantifiers, thresholds, time, obligations, a compositional grammar or a side-by-side editor. The parser works on tokens; the step from raw text to tokens is a plain split and is not itself proved.

The cost so far is two working sessions for the library and one for this essay. The cost that matters more is the one formal methods cannot remove: LangLib proves that a sentence means what its construction declares, not that the drafter chose the right construction, nor that a name such as present_183_days is defined correctly. Those remain human judgements. What changes is where they are made: once, at the point of approval, in canonical English, instead of silently each time a model reads the text.

The aim is a shared vocabulary in which people and agents agree on what a requirement means before anyone writes code against it, and in which any change to that meaning is a reviewed change to a library rather than a silent change in a model's reading.

Written with my AI research partner; the Lean library was written and kernel-checked before this essay was drafted, and every code block is taken from it. Lean 4.29.1; zero sorry; theorems depend only on Lean's standard axioms. The library currently lives in my private monorepo.

Companion: Lean-Ready English, in Lean-Ready English, the same argument written only in sentences the parser accepts, each with its Lean meaning.

Earlier: A Dictionary Whose Definitions Compile, The Legal Reasoning Wind Tunnel and Verified Specification as Code.

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.