Centre for Interdisciplinary Research in Computational Algebra (CIRCA) seminar

Peter Cameron will present Small EPPA witnesses for graphs

Abstract: A graph is homogeneous if every isomorphism between induced subgraphs extends to an automorphism. The finite homogeneous graphs were determined by Gardiner in 1976.
An EPPA witness for a graph G is a graph H containing G with the property that any isomorphism between induced subgraphs of G extends to an automorphism of H. Thus a graph is homogeneous if and only if it is its own EPPA witness. Hrushovski showed in 1992 that every finite graph has a finite EPPA witness.
Recently David Bradley-Williams, Sofia Brenner and Honza Hubička and I have determined all n-vertex graphs which have an EPPA witness with at most 2n vertices. This can be regarded as an extension of Gardiner's theorem.
A feature of the work is that we have used AI, not to prove the theorem but as an adversarial referee to pinpoint weak points in our arguments.

András Salamon will present Formalising the nondeterministic time hierarchy theorem in Isabelle with LLM assistance

Abstract: Using Claude Opus we have formalised a version of the classical nondeterministic time hierarchy theorem in 150,000 lines of Isar, verified with the Isabelle theorem prover. This theorem says that allowing nondeterministic Turing machines to use slightly more time allows strictly harder languages to be decided. I will speak about the process, useful tools developed along the way, and a little about the age of machine proofs.

Further details about this event, along with information about CIRCA, can be found on the CIRCA website https://circa.st-andrews.ac.uk