Theorem Proving in Lean - Basics of Dependent Type Theory

The master guide is here.

DTT and its Specific Variant for Lean

Dependent type theory (DTT) allows you to express complex mathematical assertions and reason about them in a "natural and uniform" way. Lean is based on a version of DTT called the Calculus of Constructions, with a "countable hierarchy of non-cumulative inverses and inductive types". This sounds complex. The following section explains this.

First, let's talk Simple Type Theory

In "type theory" every expression has a specific type. e.g. the expression x+0 may denote a natural number in a specific context. In another context, it may be a floating point number, of a particular precision.

In Lean, a natural number is an arbitrary precision unsigned integer.

An arbitrary-precision integer can grow to any number of bits, limited only by available memory. This differs from so-called fixed-width integers (8-, 32-, 64- bit).  A variable-length array of digits/bits are used so it can represent arbitrarily large integers without overflow. (Analogy: BigInt in Java, or System.Numerics.BigInteger in C#).

Let's define some constants in Lean.

/- Define some constants. -/

def  m:  Nat := 1   --m is a natural number

def  n :  Nat := 0

def  b1: Bool := true  --b1 is a Boolean

def  b2: Bool := false

Now check their types using: #check m;  #check n; #check n+0 etc. You can also run some "evals" in Lean: #eval  5*4; #eval m+2 etc.

The def keyword introduces new constant symbols to the working environment. The #check command asks Lean to report their types. The #eval command asks Lean to evaluate the given expression.

What makes simple type theory powerful is you can build new types out of others.

Theorem Proving in Lean - Three Definitions to Get Started

This is an abridged account of Theorem Proving in Lean capturing only the SSPs, or super salient points.

Here are some three starting definitions essential for understanding this topic:

Formal verification - using logical and computational methods to establish claims that are expressed in precise mathematical terms. Example claims - mathematical theorem /hypothesis, claims that pieces of hardware or software, network protocols, security protocols - do what they say they actually do.  The process is "describe your system in mathematical terms" ,then use "theorem proving" to establish truth.

Automated theorem proving - focused on "finding". The "ATP" toolkit includes: resolution theorem provers, tableau theorem provers, fast satisfiability solvers to provide means of establishing validity of formulas in propositional and first-order logic.  Computer algebra systems may be used in concert to carry out mathematical computations.  

Automated reasoning - differs; not as "cast iron" as theorem proving. Automated reasoning is a superset of automated theorem proving, which includes imprecise techniques such as heuristic search and fuzzy logic.

The Lean Programming Language

The Lean Programming language is being used to create a new proof of Fermat's Last Theorem. Some lecture notes from London's Imperial College set the scene.

Theoretical Foundation (DTT)

Dependent type theory (DTT) is the theoretical foundation of Lean (the link provided takes you into the Lean manual and gives a brief intro to the theory) which bears "categorical semantics".

Getting Started with Lean

• The best way to get started in Lean is to read Functional Programming in Lean.
• The next step is to read Theorem Proving in Lean.

Who created Lean

Lean was created by Brazilian computer scientist Leonardo de Moura, in 2013, when he worked in Microsoft Research (where he worked for 16 years). Leonardo is now Senior Principal Applied Scientist at AWS, where he works in the Automated Reasoning Group. Lean is available under the Apache 2.0 license.

ngrams, ngrams everywhere

An n-gram is a continuous sequence of n items - words, letters or symbols - from text or speech, used to analyze patterns and predict sequences in language.

Suppose we choose the items of our n-gram as "words". We then have the following taxonomy:

• unigram - consisting of a single word e.g. design
• bigram - consisting of two words e.g. design experiments
• trigram - e.g. design of experiments

Google has a great ngram viewer to see the frequency of certain ngrams in books throughout the ages.

mTLS - building machine to machine trust

What is mTLS? 

mTLS is also known as mutual TLS, after the ubiquitous security protocol. It is used in environments where machine-to-machine trust really matters.

Where in general is mTLS used? Where specifically is mTLS used? Did someone say "Kubernetes service mesh"? I think so! 

It's not generally used for public websites, but inside serious enterprise systems, it's a standard way to guarantee only authenticated services speak to each other.

Examples in modern infrastructure include: Kubernetes service meshes (Istio, Linkerd), API gateways, internal microservices, banking and trading and zero-trust networks.

Is mTLS a standard?

It's a section in TLS standard.

Root Certificates

In cryptography, a root certificate is a public key certificate that identifies a root certificate authority (CA).

Examples of certificate authorities (CAs) include SwissSign.

Root certificates are self-signed and forms the basis of an X.509-based public key infrastructure (PKI). Recall the X.509 is the ITU standard for defining the format of a public key certificate.

Worth reading also is RFC5280 which covers X.509 certificates and CRLs (certificate revocation lists).

Certificate Validation with Certifi in Python

The Python certifi package provides Mozilla's "carefully curated collection" of Root Certificates to validate the trustworthiness of SSL certificates while verifying the identify of TLS hosts. 

It has been extracted from the Requests project.