## Research

Notes about my work

My main specialty is universal algebra; current projects focus on lattice theory, computational complexity, and universal algebraic approaches to constraint satisfaction problems. Other research interests include logic, category theory, type theory, functional programming, computer-aided mathematical proof and formalization of mathematics.

My **research statement** summarizes some of my research projects. Some of that information can also be found in this post.

*Photo: Ralph Freese describes something about the 3-generated free modular lattice to JB Nation as Peter Mayr looks on. (Hawaii, May, 2018.)*

## Formal Foundations for Informal Mathematics Research

I am fascinated by the connections between programming languages and mathematics, and my most recently initiated research program aims to develop a library of all core definitions and theorems of universal algebra in the Lean proof assistant and programming language.
The title of this project is *Formal Foundations for Informal Mathematics Research* and a detailed project description is available in the document
demeo_informal_foundations.pdf.

## Bounded Lattices and Fiber Products

About a year ago I began collaborating with Peter Mayr (CU Boulder) and Nik Ruskuc (University of St. Andrews) who were interested in knowing when a homomorphism $\varphi \colon \mathbf{F} \to \mathbf{L}$ from a finitely generated free lattice $\mathbf{F}$ onto a finite lattice $\mathbf L$ has a kernel $\ker \varphi$ that is a finitely generated sublattice of $\mathbf{F}^2$. We conjectured that this could be characterized by whether or not the homomorphism is *bounded*. (See
the book by Freese, Jezek and Nation for the definition of a bounded lattice homomorphism.) and I presented a proof of one direction of this conjecture at the Algebras and Lattices in Hawaii conference earlier this year. Last month we proved the converse and thus confirmed our conjecture. All along Mayr and Ruskuc have had in mind an application for the fact that our new result is equivalent to a characterization of \emph{fiber products} of lattices. With the proof of our new characterization theorem complete, we expect to have a manuscript ready for submission by January 2019.

## Algebras and Algorithms, Structure and Complexity

In 2015, I joined a group of 8 other scientists to form a universal algebra research group and secure a 3-year NSF grant for the project, Algebras and Algorithms, Structure and Complexity Theory. Our focus is on fundamental problems at the confluence of logic, algebra, and computer science, and our main goal is to deepen understanding of how to determine the complexity of certain types of computational problems. We focus primarily on classes of algebraic problems whose solutions yield new information about the complexity of CSPs. These include scheduling problems, resource allocation problems, and problems reducible to solving systems of linear equations. CSPs are theoretically solvable, but some are not solvable efficiently. Our work provides procedures for deciding whether a given instance of a CSP is tractable or intractable, and we develop efficient algorithms for finding solutions in the tractable cases.

My work on this project culminated in a 50-page manuscript co-authored with Cliff Bergman and entitled Universal Algebraic Methods for Constraint Satisfaction Problems. This was recently accepted for publication in the journal *Logical Methods in Computer Science* (LMCS); a draft of the paper resides at arXiv cs.LO 1611.02867.