Three papers by Philippe Schlenker were checked by formalizing their definitions, lemmas and theorems in Lean 4, as a case study for the “AI for linguistics” paper. Each project records which results were proven as stated, which needed a corrected proof or statement, and what remains unformalized.
Local Contexts, Appendix: Comparing Five Theories of Presupposition Projection
The appendix's definitions, lemmas and theorems relating Transparency, local contexts, Kleene and Supervaluationist acceptability, and Heim's dynamic semantics, for the propositional fragment (plus abstract and special quantificational cases).
9 Lean files, 2124 lines.
Anti-dynamics: presupposition projection without dynamic semantics (J. Logic, Language and Information 16, 2007)
Transparency compared with Heim/Beaver dynamic semantics: Theorem 1 (propositional), Lemmas 1-2 and Theorem 2 (quantificational), the worked examples and the deviant connectives (and*, or*, unless).
15 Lean files, 3208 lines.
Iconological Semantics (Schlenker and Lamberton), geometric part, Sections 7.2-7.3
The original projection definitions (85) and (90), a reconstruction of the similarity-based formulation suggested in footnotes 45 and 64, and proofs that the two are equivalent.
2 Lean files, 871 lines.
Workflow. For each paper, the definitions, lemmas and theorems were first extracted into a
checklist (TODO.md), then formalized in Lean 4 and recorded, one row per result, in RESULTS.md
(paper location, informal statement, Lean statement, file and line, status). Each project page is generated
directly from those files; the Lean code in the expandable rows is read from the cited lines.
What worked. Formalization surfaced places where the printed argument does not go through as written (for example a missing restriction to the context in Lemma 1 of the Local Contexts appendix and a missing expressiveness hypothesis in Theorem 2 of Anti-Dynamics, plus several proof gaps and typos), in several cases together with a corrected statement that Lean accepts and a countermodel checked by computation. Claims that turned out correct are recorded as such.
Lean setup. Core Lean 4 only (no Mathlib). The per-paper notes list only the standard
axioms propext, Classical.choice and Quot.sound for the theorems checked with
#print axioms.
Categories. Every result and suggestion is placed in exactly one category, independently of how it was proved (a countermodel or a direct proof makes no difference):
Caveats.
RESULTS.md, so not distinct
theorems); suggested new results are extra cards, and one card can bundle several typos.All Lean files are in lean/, are checked by sh lean/check.sh (Lean 4.34, core only, no Mathlib), depend only on the standard axioms propext, Classical.choice, Quot.sound (checked with #print axioms). Item numbers are the appendix's (1-41); page numbers are the printed ones (p. 39 = first appendix page). File:line refer to the current files in lean/ (line of the theorem/def).
pp', not, and, or, if). The full L (predicates, generalized quantifiers, context variables c', assignment functions) is not formalised. Quantificational content is covered by (i) the abstract framework LCAbstract.lean, which is stated for arbitrary extensional environments over arbitrary D (so Lemmas 2-5, Thm 20, 21 hold for predicates too, as in the paper), (ii) the single sentence (No P . QQ') on one world with D = Fin n (Thm 38b/39b), (iii) Example 23 with D = Nat. Not covered: Theorem 2, general Theorem 22, Theorem 16(b) for full L, quantificational versions of Thm 36/38a and Lemmas 6-8.α _ β' is modelled abstractly by an environment Ψ : Val → W → Bool (semantic effect of filling the hole), and in the propositional instance by a list of frames (neg, left o G, right o F). Incremental version = same left siblings, arbitrary right siblings (Frame.same); symmetric = the actual context. For a hole that is the left operand, the connective is fixed by the frame (in the paper, β' may also change the connective). I did not prove this makes no difference; informally it does not, since the and/trivial-completion already forces the same condition (and the brute-force checks below agree).γ, d' range over all formulas (Transp) or all functions (abstract tr), i.e. Expressivity (item 3) is assumed; in the propositional bridge (bridge_i) it is the hypothesis Expressive I.W -> Prop on an arbitrary type W (no finiteness). The dynamic semantics is classical-logic-based (dyn is noncomputable).Option Bool. valOpt reads a trivalent value off the set of values attained by extensions; Super/Kleene are then exactly items 25/28 (super_eq_some_iff, kleene_eq_some_iff).k = k-th trigger, left to right) instead of per-symbol; since distinct superscripts make tokens independent, this is equivalent. Trigger symbols are pairs of letter names (a,b), so two names for the same proposition are different symbols, as in the paper.SuperAccI etc.) is as in items 26/29: all trigger occurrences, all good finals without triggers, all w ∈ C.(No P . QQ') is specialised: a single world, D = Fin n, quantifier as tree of numbers, the trigger is the whole scope, so incremental and symmetric versions coincide. Super and Kleene coincide because the trigger occurs once.Kleene = SK) were also brute-force checked in Python on random formulas over 2 and 3 worlds (lean/bruteforce_check.py, run python3 bruteforce_check.py 2 1 3000; prints {} when no counterexample is found); no discrepancy. This is exploration only, the Lean files are the proofs.All Lean files are in lean/ (lean/README.md explains how to check; lean/check.sh rebuilds from scratch). Core Lean 4 only (no Mathlib), Lean 4.34. #print axioms shows only propext, Quot.sound, and (for theorems using classical reasoning) Classical.choice.
Notation in the "Lean" column: S := sys v i0 (propositional) or sys M (quantified); S.Transp C F = Transparency; S.Def F C = C[F] ≠ #; S.Upd F C = C[F]; S.TS F C = {w ∈ C : w ⊨ F}. File:line are lean/AntiDynamics/<file>.lean:<line>.
β". Core.lean uses one-hole contexts; a completion of the initial string α is a context with the same left material, the same bracket depth, a free right material, and a free connective (and/or) where the initial string is a bare (. Strings.lean proves that this coincides with the literal string definition (strTransp_iff_transp), on the connective structure, treating each clause as one token.(Q P̲P' is . Y) (any predicate Y) and of (Q P . R̲R' is ) ("for syntactic reasons", as in the paper); this is encoded directly in lvar, not derived from a string grammar for clauses. Replacement γ in (P and γ) is an atomic predicate (P_m), as (18) allows only (P_i and P_k).p ∨ ¬p, p ∧ ¬p built from a designated letter i0. In p̲_a p'_b the presupposition a and assertion b are independent letters. Individual variables and the meta-language ∀d, ⇒, ⇔ of (18) are Lean's own, not object-language syntax.{0,…,n−1} (constant finite size built into QModel). A quantifier is given only by its tree of numbers f : ℕ → ℕ → Bool; permutation invariance, extension and conservativity are thereby built in, and no further property of f is assumed (NT supplies non-constancy). Counting is via List.range/countP (core Lean).Sys.NT), matching (28); the two conjuncts (≠ T, ≠ F) are required for the same completion, as in the paper.Infinite.lean in a self-contained semantic form (one world, γ ranging over all sets), not inside the CCP framework of QModel.and*, or*, unless are modeled as definedness/update functions over the propositional CCPs; unless is not added to the syntax (its Transparency behaviour is obtained via the static-content-equivalent or/if not).(Q P . R) with predicates P_i, P̲_iP'_k, (P_i and P_k).All Lean in lean/IconologicalGeometry.lean (checked by lean/check.sh). Page references: manuscript page numbers of source/Iconological-Semantics.pdf.
Rat replaces R (no Mathlib; the proofs are ring identities). Time is Rat. Worlds are suppressed: the lexical condition is a parameter lex.obj, cl), which the paper's (84) does not have (Issue 6).propext, Classical.choice, Quot.sound (from grind); numeric checks by kernel evaluation.