Probability in the form. of P. Freiman Ruzsa - Rémy Degenne

Stream: Lean Together 2024

[Kim Morrison]

Interesting reading re: PFR for those who haven't seen it yet: Terry wrote up a very nice blog post at https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/.

[Christopher Hoskin]

Is there any more info on how to use blueprints? The README is a bit sparse https://github.com/PatrickMassot/leanblueprint

[Chris Birkbeck]

There is a good blueprint example here: https://github.com/utensil/LeanBlueprintExample by @Utensil Song which I found very helpful

[Rémy Degenne]

I created a blueprint two weeks ago and here are the notes I took while trying to install everything. I know that Patrick updated blueprint recently, so some of it might be out of date, and some of it might just be me trying useless things. I agree that more doc would be great.
Advice: don't try to setup a blueprint on windows.

My notes

• Create a github repository (for these instructions: git@github.com:RemyDegenne/CLT.git)

• Create a lean project (locally). See https://leanprover-community.github.io/install/project.html
  -> the toolchain info in the "lake new" command from that page does not work (I may have deleted that toolchain) but "lake new" without toolchain info works.

• Upload the project to the repository. In the folder of the project:
  git remote add origin git@github.com:RemyDegenne/CLT.git
  git checkout master
  git add --all
  git commit -m "initial commit"
  git push

  Possible issues: the name of the default branch in my repository is "master", but it might be "main" in yours

• test the lean project. In the folder of the project:
  lake exe cache get
  lake build

• install latex

• install plastex http://plastex.github.io/plastex/
  pip install plasTeX

• install leanblueprint https://github.com/PatrickMassot/leanblueprint
  sudo apt install graphviz libgraphviz-dev

    on Windows: see https://pygraphviz.github.io/documentation/stable/install.html
    Don't install graphviz in a location with a space in the path
    The command that I successfully ran in git bash, after installing Graphviz in C:\Graphviz :
    pip install --global-option=build_ext --global-option="-LC:\Graphviz\lib/" --global-option="-IC:\Graphviz\include" pygraphviz

  pip install invoke pandoc

  # here: go to a folder where you are ok to clone leanblueprint
  git clone git@github.com:PatrickMassot/leanblueprint
  pip install ./leanblueprint

• setup doc-gen4 for the project https://github.com/leanprover/doc-gen4
  Follow the instructions over there.
  I failed to get the docs to build locally on Windows. See the CI step to have them built when you push.

• create a blueprint for the project
  create a folder blueprint
  Copy some files from the PFR project (adapt some names to your project)
  tasks.py
  blueprint/requirements.txt
  blueprint/tasks.py
  blueprint/.gitignore
  blueprint/src/extra_styles.css
  blueprint/src/latexmkrc
  blueprint/src/plastex.cfg
  blueprint/src/print.tex
  blueprint/src/util.sty
  blueprint/src/web.tex
  blueprint/src/chapter/main.tex
  blueprint/src/preamble/common.tex
  blueprint/src/preamble/print.tex
  blueprint/src/preamble/web.tex

• setup CI https://leanprover-community.github.io/ci.html.
  See also the PFR project CI, which can build the docs and blueprint.

  Activate "github pages" on you github repository, with deployment from github actions

useful options in the lakefile.lean file:
leanOptions := #[
⟨relaxedAutoImplicit, true⟩, -- prevents typos to be interpreted as new free variables ⟨pp.unicode.fun, true⟩, -- pretty-prints fun a ↦ b
⟨`pp.proofs.withType, false⟩]

[Patrick Massot]

A lot more documentation and a more convenient way to setup a Lean blueprint is on its way.

[Patrick Massot]

I hope the above information by Christopher and Rémy will be completely obsolete in at most two weeks.

[Terence Tao]

Someone asked in the talk for an example of a task that was easy on paper but hard in Lean. One fact, which we didn't even bother to write in the blueprint because it was so obvious, was that if one had a collection of independent random variables ,say A, B, C, D, E, then any collection of disjoint tuples of these variables, e.g., (A, C), (B, D), E, were also independent. Proving this took us through quite a bit of dependent type hell before we found a proof (which was the second to the last thing we needed to finish the main PFR objective). Later we observed that with correct spelling of the statement pfr#ProbabilityTheory.iIndepFun.pi' , the proof was actually not too bad; many of the difficulties were of our own making. Nevertheless this was a major speedbump.

Related: the very last sorry we needed to fill was

abbrev S1 : Fin 3 → Finset (Fin 4)
  | 0 => {0}
  | 1 => {1}
  | 2 => {2, 3}

example: Pairwise (Disjoint on fun x ↦ S1 x) := by sorry

Again, "obvious", but bashing this out with fin_cases etc. looked really unappealing until @Johan Commelin found this elegant proof:

example: Pairwise (Disjoint on S1) := by
  rw [pairwise_disjoint_on]
  decide