λ-cube

Introduction - Infinite search in finite time It should come as no surprise that an exhaustive search over a finite set can be performed algorithmically by enumeration. On the other hand, it is impossible to perform such an exhaustive enumeration over the natural numbers or the integers, as these sets are infinite. However, somewhat paradoxically, there are infinite sets that can be exhaustively searched in finite time. More precisely, there is at least one infinite set $X$ with the property that for any given Boolean-valued function $p$ on $X$, it is possible to algorithmically verify within finite time whether $p$ holds for all elements of $X$ or to produce a counter-example if one exists....

This post describes a way of viewing deterministic automata from a combinatorial and topological lens, as covering spaces of certain graphs. Roughly, every word over a given set of symbols can be thought of as a path on a certain graph, and the execution of the automaton can be interpreted as path lifting. A quick search of the internet does not bring up anything related, but it is possible that this connection has already been made before....

Combinatory logic Combinatory logic is a simplified model of computation based on combinators - functions that take in other functions and combine them using only function application. It was introduced by Moses Schönfinkel and rediscovered by Haskell Curry. Interestingly, combinatory logic is free of variables - every combinator can be expressed in terms of just two special combinators known as $S$ and $K$. It is possible to encode natural numbers and intuitionistic propositional logic in the language of combinators....

A general equality problem for Abelian groups Consider the problem of deciding whether of deciding whether an equation, such as $$ (x + y) + z + -(x + z) = y$$ is true in all Abelian groups. This means that for any Abelian group $A$, and for any chosen values $x$, $y$ and $z$ in $A$, the equation should be true. This hardly poses a problem, for humans atleast - by "expanding", "cancelling", "rearranging" and "grouping", anyone well-versed in high-school algebra can solve an arbitrary instance of this problem without much thought....

The Unit Conjecture The Unit Conjecture is a fundamental and well-known question about group rings that goes back to Graham Higman and Irving Kaplansky in the mid-twentieth century. It is a part of a collection of several conjectures posed by Kaplansky - most notably the Zero-divisor conjecture and the Idempotent conjecture. These are collectively known as Kaplansky's conjectures. The statement Consider a field $K$ and a group $G$. In the group ring $K[G]$, the elements of the form $k \cdot g$, where $k \in K \backslash \{0\}$ and $g \in G$, are clearly invertible - with the inverse being $k^{-1} \cdot g^{-1}$....

Introduction Mathematical objects can often be described in several ways, each description usually offering a different perspective and serving a different purpose. For example, group rings - the subject of this post - can be described in two very different ways. Given a group G and a ring R, one way to think of the group ring R[G] is as the space of functions from G to R having finite support, with addition being pointwise and multiplication given by convolution....

Introduction The Lean theorem prover is one of several that supports constructing proofs using tactics - commands that allow users to build up proofs step-by-step interactively at a high level of abstraction, usually interspersed with automation (for a demonstration of tactics and an introduction to Lean in general, consult the Natural Number Game). One of the appealing aspects of Lean, especially Lean4, is that there is a robust framework in place for users to write custom tactics within the language, making Lean its own metaprogramming language....