The Research Agenda

Thesis. The honest word for these seven topics is under-integrated, not unknown: I checked, and four have active work aimed at agents, one (interpretability certificates) has active work aimed at models and not agents, while the other two, channels through proofs and look-alikes in controlled English, sit beside live literatures not yet applied to them [empirical]. Two results recur. Canonicalising [reducing to one standard form] moves covert capacity from distinct terms to distinct meanings, and it reaches zero only where there is no choice left to make [formal]. In my small interpreter, affine and linear disciplines bound counts, not what one permitted emission says [formal], and I expect the same of session types, which fix shapes [speculative]. So my ranking is unfashionable: the cheapest two items, withholding checked proofs from later agents and gating the vocabulary file, should come first, and sheaf-based confidence probably adds little to min until someone shows otherwise [normative for the order, speculative for the sheaf guess].

The tags. [formal] means kernel-checked in this book's Lean, in lean/BuildingInSteel/Agenda.lean unless the sentence names another chapter. [formal, cited] means a proof published by someone else, which I did not check. [empirical] is something measured or observed, by me or by a named paper. [historical] says who published what, and when. [normative] is my judgement of what matters or should happen. [speculative] is a guess. A tag covers its sentence. Questions, headings and signposts carry none; the "what would settle it" lines and verdicts are all [normative], and the predictions are [speculative].

Disclosure of interest: I build AI systems for law firms, and one of the rules questioned below is mine [historical]. I gain if buyers start asking about these gaps, so discount the ranking [normative]. Every theorem here is about a small model or is a general fact about lists and functions, stated to make a question exact, and none settles a topic [normative]. The Ashdown instruction, the invented intake matter that recurs through this book, supplies the examples.

1. Covert channels inside valid proofs

Known. The Hands proved that a schema can carry a bit if and only if it accepts two different values [formal]. The demonstration this chapter owes is sharper: two terms of one type, with the same meaning downstream. Compiles, copied from Agenda.lean:

def termA : Intake := { status := .accepted, urgent := false }
def termB : Intake := { status := .accepted, urgent := true }

theorem two_terms_one_type :
    termA ≠ termB ∧ termA.meaning = termB.meaning := by decide

Here meaning reads status, because that is the field policy acts on, so urgent is spare [formal]. spare_iff_not_injective generalises this to every type and schema: a bit can pass without changing the meaning if and only if the schema holds two different values with one meaning [formal]. Canonicalise and that bit dies, but not the channel [formal]. Compiles, statement only, proof in the file:

theorem canonical_capacity_iff {V M : Type} [DecidableEq M] (meaning : V → M) (c : V → V)
    (hc : Canon meaning c) (S : List V) :
    (∃ (enc : Bool → V) (dec : V → Bool), (∀ b, enc b ∈ S) ∧ ∀ b, dec (c (enc b)) = b)
      ↔ ∃ a b, a ∈ S ∧ b ∈ S ∧ meaning a ≠ meaning b := by

After a canonicaliser that keeps meaning and merges equal meanings, a bit passes if and only if the schema holds two values of different meaning [formal]. Its "if" direction is the one-bit case of something already published: Tailor's preprint gives a lower bound growing with the logarithm of the number of policy-valid alternatives, and says "bottlenecks alone are insufficient" (Tailor, 2026) [formal, cited]. The same paper reports a maximum decoder advantage of 0.0000 in its strict lanes, which use deterministic controls, at a median 27.53 seconds per fully proved turn; 0.0500 against its adaptive attacker; and up to 0.3452 per task family in its open-model lanes [empirical]. I have not reproduced these.

Elicited collusion is measured [empirical]. Roger and Greenblatt found paraphrasing held their best schemes to no more than 3 bits per KB "under the right conditions" (Roger and Greenblatt, 2023), and Mathew and colleagues found paraphrasing and oversight "not fully effective" (Mathew et al., 2024) [empirical]. Rippin and colleagues report coding agents building stegosystems with tools, with coordination between independent agents now the main barrier (Rippin et al., 2026) [empirical]. Network security has the design pattern: Handley, Paxson and Kreibich's traffic normaliser removes ambiguity before a monitor looks, and they ask how far that undermines "end-to-end protocol semantics" (Handley et al., 2001) [historical].

A proof is a stranger case, because Lean already holds half of the answer [normative]. proofs_equal_inside is proof irrelevance as a statement, and no_decoder_inside follows: no function inside the logic can read a bit from a choice of proof [formal]. decoder_for_data shows the contrast for data [formal]. Yet proofA and proofB print as two different terms, rfl and of_decide_eq_true (id (Eq.refl true)), while proofA_eq_proofB holds by rfl [empirical for the printing, formal for the equality]. The capacity sits in the artefact and not in the mathematical object, because a receiver outside the logic reads bytes [formal for the inside, speculative for what agents would do with the outside].

Not known. I found no paper measuring a channel through accepted proofs: an arXiv metadata search for steganography, covert channels or subliminal channels with proof assistants, Lean, Coq or proof terms returned zero on 02/11/2026, and a general web search found none [empirical]. Metadata is not full text, so this is absence from my search and nothing stronger [normative]. Here the older literature has simply not been applied [speculative].

Proposal. Once a checker has accepted a proof, later agents should not see it: pass on the statement, the verdict and the axioms, and keep the text in a store for repair [normative]. Lean's own guidance supplies the checker for a different risk, proofs that cheat, and does not mention channels: it counts "un-reviewed AI-generated proofs" as malicious and describes a checker that "ensures that the proved theorem statements match those in the trusted challenge file" (Lean reference, read 02/11/2026) [historical]. With a trusted challenge, the channel falls to whether and when a proof arrived; where agents choose their own statements, canonical_capacity_iff says the choice of statement stays open [speculative]. The cost is real, since a later agent repairing a broken proof needs the text [normative].

What would settle it. Agent pairs pass random bits through Lean proofs accepted against a fixed challenge, with bits per proof reported twice: with the proof text visible to the receiver and with it withheld.

2. Canonicalisation and look-alikes in Lean-ready English

Known. Boucher and Anderson showed source that "appears different to a compiler and to the human eye" across many languages (Boucher and Anderson, 2021) [empirical]. Unicode warns of "identifiers that look like they are the same, but are actually different" (UTS #55) and specifies mixed-script detection (UTS #39) [historical]. A hostile specialist will name Wiedijk first: a prover should let the user "know what it is that the interactive theorem prover is proving", and his Pollack-consistency concerns parsing what the system printed (Wiedijk, 2012) [historical]. What follows is neighbouring and different, since the bytes survive and the reader's eye is what fails [speculative].

So I ran it. Compiles, from Agenda.lean; the second name has a Greek omicron, U+03BF:

def consent : Bool := true
def cοnsent : Bool := false

theorem twin_names_differ : consent ≠ cοnsent := by decide

The kernel sees two names and two values [formal]. Lean v4.29.1's isLetterLike admits Greek, and a bare Cyrillic а is refused with exit 1, though Lean accepts it inside guillemets, where #print shows «cаse» [empirical]. A grep of the core Lean and Init sources for "homoglyph" and "confusable" found nothing [empirical]. Mathlib's text linter does hold an allow-list, but it includes U+03BF and omits U+0430, so it should pass cοnsent (Mathlib, read 02/11/2026) [empirical].

Lean-ready English does better than I feared [empirical]. I ran seven look-alike probes through the real lrecheck binary with this book's vocabulary: a Cyrillic а in a noun, a determiner and a verb, a zero-width space, a no-break space as separator, a right-to-left override, and a decomposed é [empirical]. All seven were refused, because noun words must be in vocabulary.txt, which is ASCII today, and verbs are compiled in [empirical]. Then I added one line to a copy of the vocabulary, a look-alike аgent [empirical]. The checker exited 0 on a file where "the agent" and "the аgent" are different referents, agent#0 and аgent#2, which are hard to tell apart on a page [empirical]. Separately, a ! test line passes for the wrong reason if its only fault is a look-alike, so a negative test can be vacuous [empirical]. The script and its output are kept with the book's sources, which are private on the date of printing.

Proposal, not shipped. The checker should refuse any non-ASCII byte in .lre and vocabulary.txt, and any new vocabulary line whose UTS #39 skeleton collides with an existing word, since ASCII alone lets c1ient join client and the checker exits 0 with two referents [empirical for the run, normative for the rule]. A mixed-script check along UTS #39 lines belongs in Lean projects that accept agent-written names [normative]. A normaliser is the wrong fix, because this grammar has no accented word it needs to preserve and refusal is simpler [normative].

Not known. I do not know how much the gate buys, because ASCII leaves the general attack open: the parser resolves referents by matching words, so "a consent" and "a permission" are two things however a lawyer reads them [speculative]. The look-alike is the cheap form of a synonym split, and no character rule reaches the expensive form [speculative].

What would settle it. A red team with write access to .lre and vocabulary files changes one Lean meaning per file, and reviewers sign off with and without the gate. The number to report is how many changes pass review, split into look-alikes and ASCII synonym splits.

3. Sheaf-based confidence

Known. Fix the site. Take the discrete space on three claims, with cover {ab, bc, ca}; a section over U is a Boolean for each claim in U. This is prose: the file has Glues and support, not the presheaf [empirical]. Abramsky and Brandenburger call this presheaf the sheaf of events and note the sheaf condition is "quite trivial", because compatible partial functions glue by union (Abramsky and Brandenburger, 2011) [formal, cited]. What can fail is a family of supports [formal]. Let three reviewers each see two of Ashdown's facts, and each conclude the pair must differ. support_spec confirms the supports, marginals_full shows they agree on every overlap, and no_global_section shows no global section exists [formal]. glues_iff_even is exact for this cover: the family glues if and only if an even number of contexts say "differ", which is the Z/2 obstruction around the cycle [formal]. Reading that as a non-zero class in H¹ of the triangle is my sketch, not in the file [speculative].

Nothing here is new [historical]. Beeri, Fagin, Maier and Yannakakis showed that a schema is acyclic if and only if pairwise-consistent relations over it are always globally consistent, as Atserias and Kolaitis report it (Atserias and Kolaitis, 2020) [formal, cited]. Abramsky drew the database link himself (Abramsky, 2012) [historical]. The field is live for agents: Heng's month-old preprint has "Three views agree pairwise, yet no single world agrees with all three", and tests a sheaf condition in a runtime harness (Heng, 2026) [historical]. Huntsman, Robinson and Huntsman outline lifting model ratings of consistency to laws and jurisprudence by sheaves (Huntsman et al., 2024) [historical].

My own rule is the test case. The Elan page says confidence is "propagated as min(own, min(deps))" [historical]. minConf_copy shows that repeating the first value leaves the minimum unchanged, so copies of one source cannot raise it [formal]. no_score_of_equal_reports_detects shows that if the odd and even triangles report the same local numbers, no function of those numbers detects gluing, and min is such a function, returning 95 on 95, 95, 95 [formal].

Not known. Coherence is not confidence [normative]. The nearest evaluation I found is a repository, not a reviewed paper: on 152 hard multiple-choice questions a four-model panel's raw agreement rate predicted wrong answers better than sheaf coherence, AUC 0.852 against 0.758, while on synthetic data it beat a proxy on severity and localisation, and H¹ reached 1.000 on cycles pairwise statistics cannot see (Widman, read 02/11/2026) [empirical]. It does not test min, and I found no evaluation that does, so the honest current position is that the obstruction is real and the score is unproven [empirical]. A plain parity or join check finds this triangle's failure, and the categorical language adds nothing to it [formal for the check, normative for the verdict]. Two things might justify the language. Čech cohomology gives an obstruction that is "sufficient (but not necessary)" (Abramsky et al., 2011), and the contextual fraction is computable by linear programming and monotone under the "free" operations of a resource theory (Abramsky et al., 2017) [formal, cited]. A confidence score that free operations cannot raise is a claim stated in that framework, and whether it maps onto legal evidence is open [speculative].

Goodhart. Score agents on gluing and they can win by comparing less: path_always_glues shows that dropping one context leaves a family that always glues, whatever the remaining two contexts say [formal]. Any coherence score therefore needs a floor on the overlaps checked [normative].

What would settle it. Seed cycles of contradiction across real documents, score detection on a held-out set, and compare min against consistency radius, sheaf energy and contextual fraction with the same local checker. No gain means the sheaf was decoration for this purpose.

4. An interpretability and types bridge

Known. Gross and colleagues prove accuracy lower bounds for a small Max-of-K transformer, and report that shorter proofs "seem to require" more mechanistic understanding, with "compounding structureless errors" as the obstacle (Gross et al., 2024) [formal, cited; empirical for the comparison]. Andric states a Lipschitz composition theorem in Lean 4 lifting per-block certificates to a global deviation bound, with coverage measured on evaluated prompts (Andric, 2025) [formal, cited; empirical for the coverage]. Ladner and Althoff certify an upper bound on the faithfulness gap of replacement networks (Ladner and Althoff, 2026) [formal, cited].

Three limits stand out. Sutter and colleagues prove that under their assumptions "any neural network can be mapped to any algorithm" once alignment maps are unrestricted (Sutter et al., 2025) [formal, cited]. unrestricted_readout is a static shadow of that, with no interventions: from any injective representation a map reads out any function of the input, so a map's existence is no evidence about the network [formal]. Adolfi and colleagues find many circuit queries on multi-layer perceptrons intractable and inapproximable (Adolfi et al., 2024) [formal, cited]. Goldwasser and colleagues plant backdoors that no computationally bounded observer can detect, under their cryptographic constructions (Goldwasser et al., 2022) [formal, cited].

Not known. Most of what exists certifies numbers about behaviour [empirical]. Two results come closer: LEACE "provably prevents all linear classifiers from detecting a concept" in an erased embedding (Belrose et al., 2023), and Chen and colleagues certify consistent outputs across gender terms for 90% of test sentences at 8 transformer blocks and 12% at 10, excluding BERT as intractable (Chen et al., 2025) [formal, cited]. The first edits the model and covers linear maps only; the second is limited to small models it trained [normative]. I found no type-like statement of the form "this component's output does not depend on this fact, over this domain, under this stated class of maps" for an unedited model of useful size [empirical]. That statement is what the legal case wants, since it is a capability bound stated from inside [speculative]. I do not know whether one is reachable, and Sutter's result means the map class must be part of the type or the type says nothing [normative]. This complements the mediator-based bounds of The Hands and does not replace them, because a bound limits reach and interpretability speaks to what is being done within it [normative].

What would settle it. A published non-dependence certificate for a transformer of at least GPT-2 small's size, naming its map class, that survives an adversarial search for a dependence.

5. Substructural types for privileged context

Known. Linear logic dates from Girard (1987)90045-4), and Wadler took it to programming in Linear types can change the world! (1990) [historical]. Idris 2 (Brady, 2021) and Granule (Orchard et al., 2019) make usage quantitative [historical]. In agents, Khan's Rust crate makes double-spending a budget a compile error, and leaves "cap-soundness on the running binary" open (Khan, 2026) [empirical]. Concordat splits budgets "linearly across handoffs" (Sikaroudi, 2026), Turn's identity handles cannot be serialised (Kizito, 2026), and Jacob and colleagues use data types to separate privilege, while saying they "do not prevent manipulation through misinformation or deception" (Jacob et al., 2025) [historical]. So budgets and credentials are being typed, and Fides, CaMeL and SPA (Girrens and Wang, 2026) track document content at runtime; a linear or graded type on a privileged document's content is the unclaimed case, in what I found [empirical].

The tempting step does not follow [formal]. In my small interpreter, affine_blocks_second_read shows an affine handle cannot be read twice [formal]. affine_handle_copy_escapes shows one read still lets the secret out twice [formal]. Make the value linear too and linear_value_blocks_copy stops that plan [formal]. Then one_emission_reveals: with one read, one injective derivation and one emission, in the strictest mode, the outside still learns which secret it was [formal]. A resource theory in the sense of Coecke, Fritz and Spekkens (2014) needs something that behaves like a resource [speculative]. Knowledge read by a model is copied into its context at that moment, and no type on the document's handle reaches that copy [speculative].

Not known. What the types might truly buy is a count on the sink [speculative]. tuples_length in The Hands gives k ^ n messages for n fields over k values, so a type bounding n across a whole session would give a static total of n log2 k bits [formal for the count, speculative for the type system]. LLMbda bounds one reclassification per use, as The Hands reports [historical]. Session-wide budgets exist at runtime: OCELOT charges "a certified min-entropy cost" against a budget across a trajectory (Xie and Li, 2026), and MNC accounts for repeated disclosures (Xu et al., 2026) [historical]. Types have guaranteed a bound on release since Fuzz, for differential privacy (Reed and Pierce, 2010) [historical]. I found no static graded type stating such a budget for agents [empirical].

What would settle it. A graded type system for agent declassification, with a soundness proof, that states a session-wide bit budget and still passes a benchmark's utility test. If budgets that pass utility turn out too large to protect one privileged conclusion, the idea is dead: Ashdown's settle-or-not is one bit, as Every Query Was Allowed shows.

6. Choreographic session types for cross-firm agents

Known. Honda, Yoshida and Carbone gave the global type and its projection (2008), and Carbone and Montesi gave deadlock freedom by design for choreographies (2013) [historical]. A specialist will warn that the base is less settled than it looks: Scalas and Yoshida show that classic restrictions "in previous work have led to flawed type safety proofs" (2019) [formal, cited]. Bocchi and colleagues monitor untrusted endpoints (2017) [historical].

Agents have arrived this year [historical]. Concordat enforces a finite-state protocol on one agent, reports zero changes without the required "yes" where a standard agent made 13 in 50 tasks with one model, and lists "Projection from a global, multiparty protocol" as future work [empirical]. Pact observes that choreographies assume "cooperative participants", adds preferences and game semantics, and calls itself "preliminary" (Gopinathan et al., 2026) [historical].

My sketch makes the two legal problems visible. untold_has_no_court_view: firm A offers, firm B chooses, and A files at court only on rejection, so the court's behaviour differs by a branch nobody tells it, and plain merging gives no projection [formal]. told_still_fails: an identical notice in both branches does not help [formal]. repaired_projects passes only because the filing has gone, so the strictest rule, which is what I implemented, refused both versions of the useful protocol I tried [formal]. Then fits_prefix: every trace my monitor accepts has only accepted prefixes, so a counterparty who stops has broken nothing the monitor can see, and stopped_counterparty_fits computes one such stop [formal].

Not known. Session types assume conformance, and the other firm's agent is not mine to type, so a monitor catches deviation and cannot compel progress [normative]. Whether any global type survives contact with a real negotiation is unknown to me, because a negotiating party's best move can be one no protocol listed [speculative]. Something is lost here that I would not formalise away: a letter nobody anticipated is a legitimate move, and a session type that refuses it removes an option the client may need [normative].

What would settle it. Take a closed, form-driven exchange between two firms, such as a standard disclosure list, type it, run it across two independently built agents with an adversarial third, and count protocol failures caught, deadlocks, and real moves the type refused.

7. Liveness with deontic logic

Known. Never Breaks a Rule, Never Finishes proved deadline_is_safety and eventually_not_safety, so a dated duty can be refuted at a finite time and an undated one cannot [formal]. Chisholm's contrary-to-duty problem dates from 1963 (Chisholm), and deadlines got a deontic logic from Broersen and colleagues (2004) [historical]. Governatori's Thou Shalt is not You Will builds a paradox from one LTL formalisation of norms, and concedes it shows that "a particular formalisation based on LTL is not suitable", "not that LTL per se is not able" (Governatori, 2014) [formal, cited].

This area is active [empirical]. DeoTEL handles punctual, maintenance and achievement obligations, has a polynomial reduction to LTL for a fragment, and observes that standard until and release operators fit badly with "deadlines may never arrive" (Soldà et al., 2025) [formal, cited]. AgenticRei registers an obligation "with a deadline" and escalates, for agents, in a prototype (Joshi et al., 2026) [historical]. SLEEC rules carry within deadlines, otherwise responses and defeaters, with conflict detection and compliance verification over tock-CSP (Getir Yaman et al., 2023), SLEEC@run.time enforces them through Abstract State Machines (De Sanctis et al., 2026), and Kharraz and colleagues compare interactions by the reparations they require (2023) [historical].

The cheap formalisation fails in a way I can compute [formal]. File by tick 14; if not, tell the insurer within two ticks. The flat property "filed or notified" is exactly "not violated" (flat_iff_not_violated, general) [formal]. flat_cannot_rank computes the cost: a filing and a deliberate non-filing with notice both pass, with different normative positions [formal]. A flat monitor would report that agent green, and an agent optimising against that monitor has a free option on its primary duty [speculative]. Formalising loses something here too, because a court may weigh a late filing's excuse, and no position type captures that [normative].

Not known. This joins the chapter's neighbours: given a norm set and a model of the agent, does "every reachable prefix still have a complying or repairing continuation"? It is machine closure with repair counted as compliance [normative]. For a finite-state model and one flat LTL norm that is settled: AG E φ in memoryful CTL*, EXPSPACE-complete (Kupferman and Vardi, 2006) [formal, cited]. I cannot answer the version that matters here: I would not trust a finite-state model of a language-model agent, and conflicting norms with defeaters are not one flat formula until someone resolves them [speculative]. doomed_before_deadline and no_obeying_agent_files_ashdown in Never Breaks a Rule, Never Finishes show the failure on one case, and I have no general result [formal for the case, speculative for the rest]. SLEEC covers conflict and deadlines, with enforcement in a separate model; I found nothing that adds handover lead time, the notice a human needs before a deadline, though that rests on a search, which is weak evidence [empirical].

What would settle it. A decision procedure for a named norm fragment with conflicts and defeaters, with complexity stated, run on a real limitation or filing rule set, that finds at authoring time a doomed prefix a human drafter missed.

What exists and what is proposed

Inventory, all [formal]; #print axioms shows at most propext and Quot.sound, plus Classical.choice for unrestricted_readout. General in Agenda.lean: spare_iff_not_injective, canonical_capacity_iff, proofs_equal_inside, no_decoder_inside, support_spec, marginals_full, glues_iff_even, path_always_glues, minConf_copy, no_score_of_equal_reports_detects, unrestricted_readout, fits_prefix, flat_iff_not_violated. General over the secret on one plan: affine_blocks_second_read, affine_handle_copy_escapes, linear_value_blocks_copy, and, over injective derivations, one_emission_reveals. General over one named schema: canonIntake_is_canon. Computed on named values, and so saying nothing beyond them: the rest. These are models of my choosing, and none is linked to a deployed agent or a real session [empirical]. The probe run is the exception: it tests the real checker binary, so the gap there is only that I tried seven probes [empirical].

Who cheats

The sender is a proof-writing or drafting agent, and the receiver is a later agent that reads its files, with the kernel and a human reviewer as wardens who look at statements [speculative]. A vendor can publish "kernel-checked" while its pipeline forwards proof text between agents, and no buyer would see that without asking [speculative]. The public-interest stake is a client's fact leaving a firm while every log is green, which Every Query Was Allowed already showed for inference [normative].

Objections

"Low bandwidth means covert channels do not matter. Exfiltrate directly or not at all." For most deployments today I think that is right, and a bounded mediator should come well before any of this [normative]. But the legally sensitive payload is often very small, and one bit decided the Ashdown example in Every Query Was Allowed [normative, then formal]. Verdict: right on priority, wrong as dismissal. What would change my mind: a reproducible result that the rate through a fully checked pipeline is zero with the proof text visible, which would make my first proposal pointless.

"You tested sheaves on the smallest example and declared them decoration." Fair, and a triangle cannot speak for richer covers or graded evidence [normative]. My claim is narrower: for this confidence-scoring job the case is unmade, and that is a statement about evidence, not about sheaf theory [normative]. Verdict: the claim stands at that scope. What would change my mind: the settling experiment going against min, which would also refute my second prediction.

"A proper graded type system handles derivation. Your interpreter is a straw man." It is a toy, and derive could carry a grade [speculative]. The grade must still be assigned to a model's output, and a model's output depends on its whole context, so I expect any honest grade to be the maximum and the budget to be spent on the first call [speculative]. OCELOT is the live counter-attempt: it charges a chosen release variant, not the model's whole output; I have not run it [historical]. Verdict: open, and this is the objection I most want to lose. What would change my mind: the graded system in topic 5 with a useful budget.

"A list of seven is a grant application." Partly, since no theorem here settles a topic and I gain from attention to them [normative]. What separates it from a wish list is the settling line for each and the predictions below, either of which can embarrass me [normative]. Verdict: judge it by whether anyone, me included, runs the first two experiments. What would change my mind: both still unrun at the end of 2028 would mean this chapter was decoration too.

Sources I read as bibliographic records only: Beeri and colleagues, Chisholm, Girard, Wadler, Honda and colleagues, Carbone and Montesi, Bocchi and colleagues, Broersen and colleagues, Orchard and colleagues, Brady. Abstract only: Belrose, Girrens, Xu, Reed, Kharraz, De Sanctis, Kupferman, Atserias, Roger, Mathew, Rippin, Ladner, Adolfi, Goldwasser, Khan, Coecke, Scalas, and Abramsky's 2011 cohomology and 2017 contextual-fraction papers.

Predictions

1. By 31/12/2027, no paper or preprint will report a measured covert rate, in bits per proof, between language-model agents through proofs accepted by a proof checker such as Lean, Coq or Isabelle. Refuted by one such measurement, however small the rate.
2. By 31/12/2028, no published evaluation will show a sheaf-derived score beating the minimum of local confidences, with a stated significance test on held-out data, at detecting seeded cross-document inconsistency in legal or regulatory text. Refuted by one such evaluation, with data available for re-running.

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.