Zulip

Zulip is an open source chat platform to help distributed teams communicate effectively. The Lean community used Zulip to collaborate.

Lean Ecosystem Decoded

elan - package manager for Lean

Lake - the standard project structure and build system used in Lean

mathlib4 - the math library for LEAN

mathlib4 can be found here. It contains both programmatic infrastructure and mathematics.

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.

e.g if a and b are types, a->b denote the type of functions from a to b, a x b denotes the type of pairs consisting of an element of type a and element of type b.

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.