Blueprint for the Liquid Tensor Experiment: Introduction

Introduction

The goal of this document is to provide a detailed account of the proof of the following theorem, along side a computer verification in the Lean theorem prover.

Theorem Clausen–Scholze

Let \(0 {\lt} p' {\lt} p \le 1\) be real numbers, let \(S\) be a profinite set, and let \(V\) be a \(p\)-Banach space. Let \(\mathcal M_{p'}(S)\) be the space of \(p'\)-measures on \(S\). Then

\[ \operatorname{Ext}^i_{\operatorname{Cond}(\operatorname{Ab})}(\mathcal M_{p'}(S), V)=0 \]

for \(i \ge 1\).

This theorem appears as Theorem 2.4.15 towards the end of this document, and we will refer to it by that label.

This document consists of two parts, and there is some duplication between the two parts. The first half gives a detailed and self-contained proof of the highly technical Theorem 1.7.1. The second half is meant to be readable in a stand-alone fashion, and therefore repeats some material of the first half. It is concerned with deducing Theorem 2.4.15 from Theorem 1.7.1.

This document can be consumed in PDF format, but it is designed first and foremost for interactive reading. An online copy is available at https://leanprover-community.github.io/liquid/. This online version includes hyperlinks to the Lean code that formally verifies the proofs, as well as two dependency graphs (one for each part of the document) that visualize the global structure of the proof.

For more information about the Lean interactive proof assistant, and formal verification of mathematics, we refer to https://leanprover-community.github.io.