## Chandra-Furst-Lipton

The purpose of this 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 definitions, theorems and proofs in this repository are taken from the now classic multi-party protocols paper of Chandra-Furst Lipton.

### The target

The formal system which we are using as a target is Lean 4, a theorem prover based on the Calculus of Inductive Constructions, a dependent type theory. Lean is a project being developed at AWS and Microsoft Research by Leonardo de Moura and his team.

### Content of this project

#### Code organisation

The Lean code is contained in the directory `src/`

. The subdirectories are:

`Mathlib`

: Material missing from existing Mathlib developments`Prereqs`

: New developments to be integrated to Mathlib

### Build the Lean files

To build the Lean files of this project, you need to have a working version of Lean. See the installation instructions (under Regular install). Alternatively, click on the button below to open a Gitpod workspace containing the project.

In either case, run `lake exe cache get`

and then `lake build`

to build the project.

### Build the blueprint

See instructions at https://github.com/PatrickMassot/leanblueprint/.

### Acknowledgements

Our project builds on Mathlib. We must therefore thank its numerous contributors without whom this project couldn't even have started.

Much of the project infrastructure has been adapted from

### Source reference

`[CFL]`

: https://www.cs.umd.edu/~gasarch/BLOGPAPERS/multiparty-vdw.pdf