### Gowers and Ganesalingam

May 12, 2013

There is a series of posts at the Timothy Gowers’s blog about software that can “solve mathematical problems” which he has been working on with Mohan Ganesalingam for the last three years. The word “problems” is used here in the way a mathematician would use it – it’s really about software that can support a mathematician trying to write a proof of a theorem. The goal is for the program to write proofs that look like ones produced by a human. The experiment Gowers sets up on his blog presents several theorems with proofs written by two humans (an undergraduate and a graduate student) and one created by the program and asks the readers to guess which proofs are written  by whom. The results are truly remarkable – while I, and most of the audience, could have a good guess which proof is written by the software, I believe I could guess it only because I had known one of the three proofs was such. If a student submitted such proof as homework to me, I would have no suspicion at all.

### IsarMathLib 1.7.2

July 20, 2011

I have released a new version of IsarMathLib. It adds about 50 new lemmas, mostly in group theory and topology, leading to the following characterization of closure in topological groups:

$\overline{A} = \bigcap_{H\in \mathcal{N}_0} A+H$

Here, $\mathcal{N}_0$ is the collection of neighborhoods of zero (sets whose interior contains the neutral element of the group), and for two sets $A,B\subseteq G$ we define $A+B$ as $A+B=\{a+b | a\in A, b\in B\}$.

### Markov chains

June 5, 2009

The approach taken in the Haskell’s probability library makes it especially convenient for modeling Markov chains.
Suppose  $\{X_n\}_{n \in \mathbb{N}}$ is a Markov chain on a state space $S$. Distribution of the process $\{X_n\}_{n \in \mathbb{N}}$ is determined by the distribution of $X_0$ and the numbers $Pr(X_{n+1}=y | X_n = x)$, $x,y \in S, n \in \mathbb{N}$, called transition probabilities. For simplicity let’s consider only time-homogeneous Markov chains where these numbers don’t depend on $n$ and let’s assume that the initial distribution is a point mass, i.e. $X_0 = x_0$ for some $x_0\in S$. Then we can define a function $f: S \rightarrow Dist(S)$, where for each $x \in S$ the value $f(x)$ is a distribution on $S$ defined by $(f(x))(y) = Pr(X_{n+1}=y | X_n = x), x,y \in S, n \in \mathbb{N}$. Here $Dist(S)$ denotes the set of finitely supported nonnegative functions on $S$ that sum up to 1. Conceptually, $f(x)$ is the the distribution of the next value of the chain given the current value is $x$. This is exactly the kind of distribution-valued function that is the right hand side operand of the $\leadsto$ operation from the previous post, which corresponds to the Haskell’s  >>=  operation in the probability monad. (more…)