Representation and Formalization of Relation Algebras

Abstract relation algebras were defined by Alfred Tarski in 1941 to capture the algebraic properties of binary relations. An interesting question is whether a given relation algebra is representable as an algebra of binary relations. Donald Monk proved in 1964 that the theory of representable relation algebras is not finitely based, and Robin Hirsch and Ian Hodkinson in 2001 showed that it is an undecidable problem whether a finite relation algebra is representable. However, Roger Maddux’s concept of n-dimensional bases and Steve Comer’s one-point extension method can prove (non)representability for various small algebras. Both methods are based on a two-player game for representability, and we revisit implementations of these algorithms and apply them to relation algebras with up to 32 elements. In particular, to decide representability for all relation algebras with 16 elements, the n-dimensional bases implementation was used in 1993 to prove the nonrepresentability for the last two such algebras. Checking these proofs by hand is rather laborious but can now be done with the help of proof assistants. Lean is an interactive theorem prover that uses a formal language based on dependent type theory to represent mathematics. Its library of definitions and theorems spans many areas of mathematics, including parts of algebra, logic, order theory and category theory. Alongside, Dr. Jipsen, we develop the theory of relation algebras in the Lean proof assistant. Lean is also an efficient functional programming language, hence this is a useful platform for implementing algorithms and checking mathematical results obtained by computer calculations. We report on the current state of our project without assuming any background about Lean.