ACC Seminar: Automated Deduction in the Exploration of Andrews-Curtis Conjecture

Abstract blocks of math formulas in virtual space in pink letters on a black background

Department of Mathematical Sciences

Location: Zoom

Speaker: Dr Alexei Lisitsa, Senior Lecturer, University of Liverpool

Refreshments will be served at 4:00 PM.

ABSTRACT

The Andrews-Curtis conjecture (ACC) is one of the most well-known open problems in combinatorial group theory. In short, it states that every balanced presentation of the trivial group can be transformed into a trivial presentation by a sequence of simple transformations. Various computational approaches have been proposed for the efficient search of such simplifications. Still, there are infinite families of balanced trivial group presentations which remain potential counterexamples to the conjecture, that is, for which the required simplifications are not known. In this talk we will discuss an approach that leverages automated deduction in first-order logic to search for Andrews-Curtis simplifications. The approach is very competitive:

1) For all proposed potential counterexamples where non-trivial AC-simplifications were found using specialized search algorithms, AC-simplifications can also be discovered using generic theorem proving technique

2) Many new simplifications were demonstrated.

The talk is based on recent publications/preprints (and references therein):

https://www.sciencedirect.com/science/article/pii/S2666657X2400034X

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=5100345

https://arxiv.org/pdf/2501.18601

BIOGRAPHY

Alexei Lisitsa

Dr Alexei Lisitsa has graduated in Mathematics from Moscow State University (1987). In 1987-1999 he has been a researcher in the Program Systems Research Institute of Russian Academy of Sciences. His PhD thesis (Russian Academy of Science, 1997) was on descriptive complexity and definability in AI and Database Theory. In 1999-2000 Alexei was a postdoc researcher in Computer Laboratory, Cambridge, and since 2001 he is affiliated with the University of Liverpool. Currently he is a Senior Lecturer in the Department of Computer Science and Director of Postgraduate Research. His current research interests include: Applications of Automated Reasoning to Mathematics and Computer Science, Automated Verification and Security.

A campus map is available at https://tour.stevens.edu.
Additional information is available at https://web.stevens.edu/algebraic/.

Zoom Link:

https://stevens.zoom.us/j/93228680142 (Password: ACC)