lean-liquid

KO | EN

gitlite — search

#javascript #python #ai #llm #machine-learning #rust #deep-learning #linux #nodejs #java #windows #kubernetes #ios #mcp

(★ 249)

💧 Liquid Tensor Experiment

File Explorer

Download Latest Version (.zip)

- - build.yml
  - nolints.yml
  - upgrade_lean.yml
- copyright.code-snippets
- settings.json
- delta_functor.lean
- extr.lean
- extr_backup.lean
- multilinear.lean
- prepresentation.lean
- sheafification_mono.lean
- count_sorry.sh
- detect_errors.py
- ensure_lte_sorry_free.py
- ensure_thm95_sorry_free.py
- fetch_olean_cache.sh
- get-cache.sh
- lean_version.lean
- lint_project.lean
- mk_all.sh
- nolints.txt
- print_lte_axioms.lean
- print_thm95_axioms.lean
- project_stats.py
- update_nolints.sh
- - apply_Pow.lean
  - category.lean
  - constants.lean
  - eg.lean
  - eval.lean
  - eval1half.lean
  - eval2.lean
  - eval_Pow_functor_nat_trans_compatibility.lean
  - FILES.md
  - functorial_map.lean
  - homotopy.lean
  - main.lean
  - suitable.lean
  - universal_map.lean
- - default.lean
  - finite.lean
  - lem97.lean
  - partition.lean
  - profinite.lean
  - profinite_setup.lean
- - ab.lean
  - ab4.lean
  - ab5.lean
  - acyclic.lean
  - adjunctions.lean
  - adjunctions2.lean
  - adjunctions_module.lean
  - basic.lean
  - bd_lemma.lean
  - bd_ses.lean
  - bd_ses_aux.lean
  - condensify.lean
  - coproducts.lean
  - evaluation_homology.lean
  - exact.lean
  - filtered_colimits.lean
  - filtered_colimits_commute_with_finite_limits.lean
  - is_iso_iff_extrdisc.lean
  - is_proetale_sheaf.lean
  - kernel_comparison.lean
  - proetale_site.lean
  - projective_resolution.lean
  - projective_resolution_module.lean
  - Qprime_isoms.lean
  - Qprime_isoms2.lean
  - rescale.lean
  - sheafification_homology.lean
  - sheafification_mono.lean
  - short_exact.lean
  - tensor.lean
  - tensor_short_exact.lean
  - top_comparison.lean
- - cond.lean
  - Ext.lean
  - pBanach.lean
  - radon_measures.lean
  - real.lean
- - default.lean
  - int.lean
  - nnreal.lean
  - normed_group.lean
- - ab4.lean
  - ab5.lean
  - ab52.lean
  - abelian_category.lean
  - abelian_group_object.lean
  - acyclic.lean
  - AddCommGroup.lean
  - AddCommGroup_instances.lean
  - additive_functor.lean
  - arrow_preadditive.lean
  - bicartesian.lean
  - bicartesian2.lean
  - bicartesian3.lean
  - bicartesian4.lean
  - cech.lean
  - chain_complex_cons.lean
  - chain_complex_exact.lean
  - colim_preserves_colimits.lean
  - commsq.lean
  - CompHaus.lean
  - complex_extend.lean
  - composable_morphisms.lean
  - concrete_equalizer.lean
  - coprod_op.lean
  - derived_functor.lean
  - derived_functor_zero.lean
  - embed_preserves_colimits.lean
  - ennreal.lean
  - equalizers.lean
  - equivalence_additive.lean
  - exact_filtered_colimits.lean
  - exact_functor.lean
  - exact_lift_desc.lean
  - exact_seq.lean
  - exact_seq2.lean
  - exact_seq3.lean
  - exact_seq4.lean
  - ext.lean
  - Ext_quasi_iso.lean
  - fin_functor.lean
  - Fintype.lean
  - fintype_induction.lean
  - free_abelian_exact.lean
  - free_abelian_group.lean
  - free_abelian_group2.lean
  - FreeAb.lean
  - Gordan.lean
  - has_homology.lean
  - has_homology_aux.lean
  - hom_single_iso.lean
  - hom_single_iso2.lean
  - homological_complex.lean
  - homological_complex2.lean
  - homological_complex_abelian.lean
  - homological_complex_equiv_functor_category.lean
  - homological_complex_map_d_to_d_from.lean
  - homological_complex_op.lean
  - homological_complex_shift.lean
  - homology.lean
  - homology_exact.lean
  - homology_iso.lean
  - homology_iso_Ab.lean
  - homology_iso_datum.lean
  - homology_lift_desc.lean
  - homology_map.lean
  - homology_map_datum.lean
  - homotopy_category.lean
  - homotopy_category_coproducts.lean
  - homotopy_category_functor_compatibilities.lean
  - homotopy_category_lemmas.lean
  - homotopy_category_op.lean
  - homotopy_category_pretriangulated.lean
  - horseshoe.lean
  - imker.lean
  - int.lean
  - internal_hom.lean
  - is_biprod.lean
  - is_iso_iota.lean
  - is_iso_neg.lean
  - is_locally_constant.lean
  - is_quasi_iso.lean
  - is_quasi_iso_sigma.lean
  - kernel_comparison.lean
  - les_homology.lean
  - limit_flip_comp_iso.lean
  - map_to_sheaf_is_iso.lean
  - mapping_cone.lean
  - module_epi.lean
  - monoidal_category.lean
  - nat_iso_map_homological_complex.lean
  - nat_trans.lean
  - neg_one_pow.lean
  - nnrat.lean
  - nnreal.lean
  - nnreal_int_binary.lean
  - nnreal_nat_binary.lean
  - nnreal_to_nat_colimit.lean
  - order.lean
  - pi_induced.lean
  - pid.lean
  - pow_functor.lean
  - preadditive_yoneda.lean
  - preserves_exact.lean
  - preserves_finite_limits.lean
  - preserves_limits.lean
  - presieve.lean
  - product_op.lean
  - projective_replacement.lean
  - projectives.lean
  - pullbacks.lean
  - quotient_map.lean
  - random_homological_lemmas.lean
  - rational_cones.lean
  - real.lean
  - salamander.lean
  - SemiNormedGroup.lean
  - SemiNormedGroup_ulift.lean
  - sheaf.lean
  - sheafification_equiv_compatibility.lean
  - sheafification_mono.lean
  - SheafOfTypes_sheafification.lean
  - short_complex.lean
  - short_complex_colimits.lean
  - short_complex_functor_category.lean
  - short_complex_homological_complex.lean
  - short_complex_projections.lean
  - short_exact.lean
  - short_exact_sequence.lean
  - single_coproducts.lean
  - snake_lemma.lean
  - snake_lemma2.lean
  - snake_lemma3.lean
  - snake_lemma_naturality.lean
  - snake_lemma_naturality2.lean
  - split_exact.lean
  - sum_str.lean
  - topology.lean
  - triangle.lean
  - triangle_shift.lean
  - truncation.lean
  - truncation_Ext.lean
  - tsum.lean
  - two_step_resolution.lean
  - types.lean
  - unflip.lean
  - whisker_adjunction.lean
  - wide_pullback_iso.lean
  - yoneda.lean
  - yoneda_left_exact.lean
- - acyclic.lean
  - basic.lean
  - epi.lean
  - lemmas.lean
  - main.lean
  - mono.lean
  - setup.lean
- - asyncI.lean
  - by_exactI_hack.lean
  - type_pow.lean
- - basic.lean
  - functor.lean
  - ses.lean
- - aux_lemmas.lean
  - basic.lean
  - bounded.lean
  - condensed.lean
  - ext.lean
  - functor.lean
  - int_nat_shifts.lean
  - no_longer_needed_maybe.lean
  - prop72.lean
  - ses.lean
  - ses2.lean
  - simpler_laurent_measures.lean
  - theta.lean
  - thm69.lean
- - basic.lean
  - bounded.lean
  - ext.lean
  - ext_aux1.lean
  - ext_aux2.lean
  - ext_aux3.lean
  - ext_aux4.lean
  - ext_preamble.lean
  - finsupp_instance.lean
  - functor.lean
  - iota.lean
  - kernel_truncate.lean
  - Lbar_le.lean
  - nnnorm_add_class.lean
  - pseudo_normed_group.lean
  - README.md
  - ses.lean
  - squares.lean
  - sum_nnnorm.lean
  - torsion_free_condensed.lean
  - torsion_free_profinite.lean
- - analysis.lean
  - completion.lean
  - completion_aux.lean
  - FILES.md
  - SemiNormedGroup.lean
  - Vhat.lean
- - basic.lean
  - compare.lean
- - controlled_exactness.lean
  - FILES.md
  - normed_with_aut.lean
  - pseudo_normed_group.lean
- - lp.lean
- - basic.lean
  - category.lean
  - cech.lean
  - cosimplicial.lean
  - cosimplicial_extra.lean
  - FILES.md
  - finsupp.lean
  - Hom.lean
  - int.lean
  - pseudo_normed_group.lean
  - quotient.lean
  - topology.lean
- - completion.lean
  - strict_complex_iso.lean
- - concrete.lean
  - extension_profinite.lean
  - prop_92.lean
- - basic.lean
  - bounded_limits.lean
  - breen_deligne.lean
  - CLC.lean
  - FILES.md
  - FP.lean
  - FP2.lean
  - homotopy.lean
  - LC.lean
  - profinitely_filtered.lean
  - QprimeFP.lean
  - splittable.lean
  - sum_hom.lean
  - system_of_complexes.lean
  - system_of_complexes2.lean
  - Tinv.lean
  - with_Tinv.lean
- - defs.lean
  - LC_comparison.lean
  - LC_limit.lean
  - main.lean
  - png.lean
  - png_reflects_limits.lean
  - setup.lean
- - basic.lean
  - condensed.lean
  - default.lean
- - basic.lean
  - CLC.lean
  - FiltrationPow.lean
  - LC.lean
  - normed_group.lean
  - polyhedral_lattice.lean
  - pseudo_normed_group.lean
  - Tinv.lean
- - basic.lean
  - completion.lean
  - double.lean
  - FILES.md
  - rescale.lean
  - shift_sub_id.lean
  - truncate.lean
- - col_exact.lean
  - col_exact_prep.lean
  - default.lean
  - double_complex.lean
  - homotopy.lean
  - modify_complex.lean
  - pfpng_iso.lean
  - polyhedral_iso.lean
  - row_iso.lean
- banach.lean
- challenge.lean
- challenge_notations.lean
- challenge_prerequisites.lean
- liquid.lean
- normed_snake.lean
- normed_snake_dual.lean
- normed_spectral.lean
- prop819.lean
- statement.lean
- VhatLbar.svg
.gitignore
.gitpod.yml
leanpkg.toml
README.md

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# Liquid Tensor Experiment

[![](https://github.com/leanprover-community/lean-liquid/actions/workflows/build.yml/badge.svg?branch=master)](https://github.com/leanprover-community/lean-liquid/actions/workflows/build.yml)
[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/lean-liquid)

For the eponymous blogpost by Peter Scholze which started it all: see https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/.

The main aim of this community-owned repository is to *digitise* some mathematical definitions, theorem statements and theorem proofs. Digitisation, or formalisation, is a process where the source material, typically a mathematical textbook or a pdf file or website or video, is transformed into definitions in a target system consisting of a computer implementation of a logical theory (such as set theory or type theory).

## The source

The main "source" definitions, theorems and proofs in this repository are all taken from Scholze's Bonn lecture notes [Analytic.pdf](https://www.math.uni-bonn.de/people/scholze/Analytic.pdf) explaining some of his work with Clausen on the theory of solid and liquid modules, and on their development of a new approach to certain proofs in complex analytic geometry.

## The target

The formal system which we are using as a target system is Lean's dependent type theory. Lean is a project being developed at Microsoft Research by Leonardo de Moura and his team. Our formalisation could not have even started without a major classical mathematical library backing it up, and so we chose Lean 3 as the engine behind the project. Although Lean 4's type theory is the same as Lean 3's type theory, it currently lacks the mathematical infrastructure needed for this project.

## Brief overview of the project

The challenge in the blog post is to formalise its `Theorem 1.1`, a variant of `Analytic 9.1` (i.e. Theorem 9.1 of [`Analytic.pdf`](https://www.math.uni-bonn.de/people/scholze/Analytic.pdf)) in Lean.

When the project started, it was immediately noticed that there was a "sub-boss" in the form of `Analytic 9.4`, a far more technical theorem involving a completely different class of objects and which Scholze was claiming was a sufficiently powerful stepping stone. The project then split into two sub-projects:
"Prove `Analytic 9.4`" and "Prove that `Analytic 9.4` implies `Theorem 1.1`"

An important intermediate achievement was the completion of a [blueprint](https://leanprover-community.github.io/liquid/) for the proof of `9.4` and the related `9.5`. The blueprint was a guide which was comprehensible to mathematicians who had no Lean training, whilst also being a visual guide to where progress was needed during the formalisation process.

The preliminary announcement of a proof of Theorem 9.4 was made on 28th May 2021, by Johan Commelin and his team from the Lean prover community.
The second half of the project was [completed](https://leanprover-community.github.io/blog/posts/lte-final/) on 14th July 2022.
Together, the two components give a formal verification of Theorem 1.1 of the blogpost.

## The formal statement of `Analytic 9.4`

The statement can be found in [`src/liquid.lean`](https://github.com/leanprover-community/lean-liquid/blob/master/src/liquid.lean#L37)

```lean
theorem first_target :
  ∀ m : ℕ, ∃ (k K : ℝ≥0) [fact (1 ≤ k)] (c₀ : ℝ≥0),
  ∀ (S : Type) [fintype S] (V : SemiNormedGroup.{0}) [normed_with_aut r V],
    ((BD.data.system κ r V r').obj (op $ of r' (Lbar r' S))).is_weak_bounded_exact k K m c₀ := _
```

See [`src/liquid.lean`](https://github.com/leanprover-community/lean-liquid/blob/master/src/liquid.lean#40)
for details on how to read this statement.

## The formal statement of `Theorem 1.1`

The statement can be found in [`src/challenge.lean`](https://github.com/leanprover-community/lean-liquid/blob/master/src/challenge.lean#L28)

```lean
variables (p' p : ℝ≥0) [fact (0 < p')] [fact (p' < p)] [fact (p ≤ 1)]

theorem liquid_tensor_experiment (S : Profinite.{0}) (V : pBanach.{0} p) :
  ∀ i > 0, Ext i (ℳ_{p'} S) V ≅ 0 :=
```

## How to browse this repository

### Blueprint

Below we explain how to engage with the Lean code directly.
We also provide a [blueprint](https://leanprover-community.github.io/liquid/)
including two [dependency](https://leanprover-community.github.io/liquid/dep_graph_section_1.html)
[graphs](https://leanprover-community.github.io/liquid/dep_graph_section_2.html)
of the main ingredients in the repository.
All material in the blueprint is cross-referenced with the Lean formalization using hyperlinks.

### Getting the project

At the moment, we support two ways of browsing this repository:
Either via Gitpod or by using a Lean development environment.

Crucially, both methods will allow you to introspect Lean's "Goal state" during proofs,
and easily jump to definitions or otherwise follow paths through the code.

Gitpod provides an online Lean environment, but requires a GitHub account
and might have weaker performance than a local installation.
To use it, simply click the Gitpod button at the top of this Readme file.

To install a Lean development environment on your computer please use the
[installation instructions](https://leanprover-community.github.io/get_started.html#regular-install)
to install Lean and a supporting toolchain.
After that, download and open a copy of the repository
by executing the following command in a terminal:
```
leanproject get lean-liquid
code lean-liquid
```
For detailed instructions on how to work with Lean projects,
see [this](https://leanprover-community.github.io/install/project.html). The script `scripts/get-cache.sh`
in the folder `lean-liquid` will download the `olean` files created by our continuous integration. This
will save you some time by not having to do `leanproject build`.

### Reading the project

With the project opened in VScode,
you are all set to start exploring the code.
There are two pieces of functionality that help a lot when browsing through Lean code:

* "Go to definition": If you right-click on a name of a definition or lemma
  (such as `Lbar`, or `Tinv_continuous`), then you can choose "Go to definition" from the menu,
  and you will be taken to the relevant location in the source files.
  This also works by `Ctrl`-clicking on the name.
* "Goal view": in the event that you would like to read a *proof*,
  you can step through the proof line-by-line,
  and see the internals of Lean's "brain" in the Goal window.
  If the Goal window is not open,
  you can open it by clicking on one of the icons in the top right hand corner.

### Important files in the project

* All the Lean code (the juicy stuff) is contained in the directory `src/`.
* The file `src/challenge.lean` contains the statement of the main theorem.
* The file `src/liquid.lean` contains the statement of the first target (the first half of the project).
* The directory `src/examples/` contains Lean files that explain the main ingredients in the statement of the main theorem.
  These files should form convincing evidence that we did not make a mistake in formalizing the necessary definitions.
* The directory `src/for_mathlib/` contains preliminary material that is gradually being moved to mathlib, the main library of mathematics for Lean.

## Brief note on type theory

Lean is based on type theory,
which means that some things work slightly differently from set theory.
We highlight two syntactical differences.

* Firstly, the element-of relation (`∈`) plays no fundamental role.
  Instead, there is a typing judgment (`:`).

This means that we write `x : X` to say that "`x` is a term of type `X`"
  instead of "`x` is an element of the set `X`".
  Conveniently, we can write `f : X → Y` to mean "`f` has type `X → Y`",
  in other words "`f` is a function from `X` to `Y`".

* Secondly, type theorists do not use the mapsto symbol (`↦`),
  but instead use lambda-notation.
  This means that we can define the square function on the integers via
  `λ x, x^2`, which translates to `x ↦ x^2` in set-theoretic notation.
  For more information about `λ`, see the Wikipedia page on
  [lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus).

For a more extensive discussion of type theory,
see the dedicated
[page](https://leanprover-community.github.io/lean-perfectoid-spaces/type_theory.html)
on the perfectoid project website.

## Source reference

`[Analytic]` : http://www.math.uni-bonn.de/people/scholze/Analytic.pdf

[Analytic]: http://www.math.uni-bonn.de/people/scholze/Analytic.pdf

lean-liquid

File Explorer

Today's picks

Was this content helpful?

Recent Feedback

lean-liquid

File Explorer

Today's picks

Was this content helpful?

Recent Feedback

Download README