# UCL MATH0109 Theorem Proving in Lean Notes

1. Introduction 2. Foundations 2.1 A_functions exact if your goal is ⊢ A and you have a term x : A, then exact x will close the goal sorry this tactic closes the...

Zhiyu Wang

1. Introduction 2. Foundations 2.1 A_functions exact if your goal is ⊢ A and you have a term x : A, then exact x will close the goal sorry this tactic closes the...

Introduction Riesz’s representation theorem is a powerful result in functional analysis, particularly in the study of Hilbert spaces. It characterizes continuous linear functionals in terms of the...

Introduction In this post, we look at identities built from vector operators. These operators behave both as vectors and as differential operators, so that the usual rules of taking the derivative...

Basics Definition 0.1 (Chromatic number) The chromatic number of a graph $G$ is defined as [\chi(G) = \text{min}{k \geq 1 ~ ~ G \text{ is } k \text{-colourable}}.] R...

I recently leveled up my Mac terminal for convenience and fun. Here is how I did it. Install Homebrew In your command line, type the following: /bin/bash -c "$(curl -fsSL https://raw.githubusercon...

Packages We first import necessary packages: numpy is the main package for scientific computing with Python. matplotlib is a library to plot graphs in Python. h5py is a Pythonic interface to...

As the days stretch on, my thoughts often wander back to the cherished moments spent at the Hicks Building at University of Sheffield, where everyone can unapologetically show the love of mathemati...

Let’s play a game with integer sequences. Observe the following sequence: [\begin{align} 1 11 21 1211 111221 312211 \vdots \end{align}] Can you tell the next number? ...

Motivation Recently, I came across an interesting application of the Lovász Local Lemma, a fundamental technique in the “probabilistic method” and a classic example of a non-constructive approach i...

Introduction There are, in general, two ways to construct things in mathematics. On the one hand, we can construct things explicitly, which tends to be difficult, if we don’t know exactly what the ...