Lean-Ready English, in Lean-Ready English
Companion to Lean-Ready English. Every sentence below is accepted by the LangLib parser. Tap a sentence to see its meaning in Lean; the small labels link each sentence to the one it builds on.
What this page is
1 First, this page is a second version of an essay.
assertion
is "this page" "second version of an essay#0"
2 Every sentence on this page is a Lean-ready sentence.
universal
∀ e, is e "sentence on this page" → is e "Lean-ready sentence#1"
3 A build check reads each sentence on this page.
assertion
reads "build check#2" "each sentence on this page"
4 The build check fails if one sentence is rejected.
sufficient condition
(is "one sentence" "rejected") → (fails "build check#2")
5 Then, the build check passed. comes after 4
assertion
passed "build check#2"
6 Each sentence has a Lean meaning beside it.
assertion
has "each sentence" "Lean meaning beside it#3"
7 You read the English and Lean reads the meaning.
conjunction
(read "you" "the English") ∧ (reads "Lean" "the meaning")
8 This version adds a narrative thread.
assertion
adds "this version" "narrative thread#4"
The problem
9 First, a language model reads a rule.
assertion
reads "language model#5" "rule#6"
10 Then, the language model guesses the meaning of the rule. comes after 9
assertion
guesses "language model#5" "the meaning of the rule"
11 So a wrong guess becomes a precise mistake. follows from 10
assertion
becomes "wrong guess#7" "precise mistake#8"
12 A precise mistake looks trustworthy but the precise mistake is still a mistake.
assertion
looks "precise mistake#9" "trustworthy"
assertion
is "precise mistake#9" "still a mistake"
13 So this page proposes a fix. follows from 12
assertion
proposes "this page" "fix#10"
The idea
14 First, Lean is a proof assistant.
assertion
is "Lean" "proof assistant#11"
15 A proof assistant checks each step of a proof.
assertion
checks "proof assistant#12" "each step of a proof"
16 Lean-ready English is a controlled form of English.
assertion
is "Lean-ready English" "controlled form of English#13"
17 Every Lean-ready sentence has one declared meaning.
universal
∀ e, is e "Lean-ready sentence" → has e "one declared meaning"
18 For example, this sentence has one declared meaning. example of 17
assertion
has "sentence 18" "one declared meaning"
19 Mathlib is the library of mathematics for Lean.
assertion
is "Mathlib" "the library of mathematics for Lean"
20 LangLib is like Mathlib for sentence patterns.
assertion
is "LangLib" "like Mathlib for sentence patterns"
21 The parser rejects an unknown pattern.
assertion
rejects "the parser" "unknown pattern#14"
22 So a rejected sentence never gets a meaning. follows from 21
negation
¬ gets "rejected sentence#15" "meaning#16"
23 No language model decides the meaning of a sentence.
prohibition over a kind
∀ e, is e "language model" → ¬ decides e "the meaning of a sentence"
24 A person must approve each meaning.
obligation
must (approve "person#17" "each meaning")
How a sentence works
25 First, each sentence has a subject.
assertion
has "each sentence" "subject#18"
26 Then, a verb follows the subject. comes after 25
assertion
follows "verb#19" "subject#18"
27 Then, an object follows the verb. comes after 26
assertion
follows "object#20" "verb#19"
28 The lexicon lists each verb.
assertion
lists "the lexicon" "each verb"
29 A noun phrase never contains a verb.
negation
¬ contains "noun phrase#21" "verb#22"
30 Each noun phrase names one thing.
assertion
names "each noun phrase" "one thing"
31 Each rendered meaning is a new sentence.
assertion
is "each rendered meaning" "new sentence#23"
32 Then, the parser reads the new sentence and the parser gives back the same meaning. comes after 31
conjunction
(reads "the parser" "new sentence#23") ∧ (gives "the parser" "back the same meaning")
33 The round-trip theorem proves that property for each sentence of the grammar.
assertion
proves "the round-trip theorem" "that property for each sentence of the grammar"
A narrative thread
34 Then, this version adds four connectives. comes after 33
assertion
adds "this version" "four connectives"
35 A reason connective marks support.
assertion
marks "reason connective#24" "support"
36 A contrast connective marks a contrast.
assertion
marks "contrast connective#25" "contrast#26"
37 An instance connective links an instance to a general rule.
assertion
links "instance connective#27" "instance to a general rule#28"
38 An order connective marks a sequence of steps.
assertion
marks "order connective#29" "sequence of steps#30"
39 Every connective keeps the meaning of each sentence.
universal
∀ e, is e "connective" → keeps e "the meaning of each sentence"
40 For example, the reason connective keeps the meaning of each sentence. example of 39
assertion
keeps "reason connective#24" "the meaning of each sentence"
41 The discourse graph never contains a cycle because every link points to an earlier sentence.
negation
¬ contains "the discourse graph" "cycle#31"
universal
∀ e, is e "link" → points e "to an earlier sentence"
42 A named referent links two noun phrases.
assertion
links "named referent#32" "two noun phrases"
43 First, an applicant introduces a referent.
assertion
introduces "applicant#33" "referent#34"
44 Then, the applicant names that referent. comes after 43
assertion
names "applicant#33" "that referent"
Conditions
45 First, the applicant qualifies if the applicant was present for 183 days.
sufficient condition
(was "applicant#33" "present for 183 days") → (qualifies "applicant#33")
46 That sentence states a sufficient condition.
assertion
states "sentence 46" "sufficient condition#35"
47 Then, the applicant qualifies only if the applicant was present for 183 days. comes after 46
necessary condition
(qualifies "applicant#33") → (was "applicant#33" "present for 183 days")
48 That sentence states a necessary condition.
assertion
states "sentence 48" "necessary condition#36"
49 These two sentences state different rules because Lean proves the difference.
assertion
state "these two sentences" "different rules"
assertion
proves "Lean" "the difference"
50 Then, the applicant qualifies if and only if the applicant was present for 183 days. comes after 49
if and only if
(qualifies "applicant#33") ↔ (was "applicant#33" "present for 183 days")
51 That sentence states both conditions.
assertion
states "sentence 52" "both conditions"
The correction
52 So an earlier essay needs a correction. follows from 51
assertion
needs "earlier essay#37" "correction#38"
53 The earlier essay tested a legal translator.
assertion
tested "earlier essay#37" "legal translator#39"
54 The earlier essay treated five wordings as one rule.
assertion
treated "earlier essay#37" "five wordings as one rule"
55 The main essay quotes the five wordings.
assertion
quotes "the main essay" "the five wordings"
56 Wording one states a sufficient condition but wording three states a necessary condition.
assertion
states "wording one" "sufficient condition#40"
assertion
states "wording three" "necessary condition#41"
57 Wording two grants a power to an authority.
assertion
grants "wording two" "power to an authority#42"
58 The parser rejects wording three as written.
assertion
rejects "the parser" "wording three as written"
59 Every rejected wording lacks a declared meaning.
universal
∀ e, is e "rejected wording" → lacks e "declared meaning#43"
60 For example, wording three lacks a declared meaning. example of 59
assertion
lacks "wording three" "declared meaning#44"
61 The word unless lacks a definition.
assertion
lacks "the word unless" "definition#45"
Real requirements
62 Then, three real requirements were restated in Lean-ready English. comes after 61
assertion
were "three real requirements" "restated in Lean-ready English"
63 These requirements have fourteen criteria.
assertion
have "these requirements" "fourteen criteria"
64 Ten criteria parse but four criteria fail.
assertion
parse "ten criteria"
assertion
fail "four criteria"
65 Every failure names a missing pattern.
universal
∀ e, is e "failure" → names e "missing pattern#46"
66 For example, one failure names a measured threshold. example of 65
assertion
names "one failure" "measured threshold#47"
67 So these missing patterns are next. follows from 66
assertion
are "these missing patterns" "next"
Limits
68 First, LangLib gives each sentence one meaning.
assertion
gives "LangLib" "each sentence one meaning"
69 LangLib never checks the intent of the author.
negation
¬ checks "LangLib" "the intent of the author"
70 So a person must approve the choice of words. follows from 69
obligation
must (approve "person#48" "the choice of words")
71 The grammar is small.
assertion
is "the grammar" "small"
72 The grammar covers simple sentences but a complex sentence needs a new pattern.
assertion
covers "the grammar" "simple sentences"
assertion
needs "complex sentence#49" "new pattern#50"
73 Every new pattern needs a theorem.
universal
∀ e, is e "new pattern" → needs e "theorem#51"
This page
74 Then, this page is a test of the idea on real readers. comes after 73
assertion
is "this page" "test of the idea on real readers#52"
75 The idea is practical if real readers follow this page.
sufficient condition
(follow "real readers" "this page") → (is "the idea" "practical")
How this page is made. The sentences live in one Lean file. One build check proves, in the Lean kernel, that every line parses, that every word inside a noun phrase is in the declared vocabulary, that every "the X" refers back to an earlier "a X" or "an X" (or to a declared name such as "the parser"), that every link points to an earlier sentence, and that every section opens with first, then or so. One rejected line fails the build. A separate theorem proves that a connective never changes what a sentence means: a line joined with because or but asserts exactly its two sentences. The links are the narrative thread: "then" marks order, "so" marks what follows from the sentence before, "because" marks a reason, "but" a contrast, and "for example" an instance of the latest general rule (checked only to the extent that the example uses the same verb as the rule). Numbers like applicant#32 in the Lean meanings are resolved referents. Headings, links, numbers and this note are page furniture; the page adds a capital letter, a comma after a lead connective and a full stop, and changes nothing else.
Read the full essay: Lean-Ready English.
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.