Joint AIAI/ DReaM Group Seminar: Monday 2nd November 2026 by Andras Salamon

Title: Formalising the time hierarchy theorems in Isabelle/HOL with LLMs

Speaker: András Salamon.  School of Computer Science, St Andrews.

Abstract: "It remains an open problem, how to [formalise] complexity theory without dying in the details" Yannick Forster, Simons Institute, April 2025

During 2026 our team completed proofs of the deterministic and nondeterministic time hierarchy theorems in Isabelle/HOL, using extensive LLM proof engineering assistance; the latter proof is new and was designed to ease formalisation and further extensions. These results say that access to only slightly more time allows strictly larger classes of languages to be recognised. The tedious Turing machine instruction tracing required for the "obvious" parts of these theorems (usually omitted as "easy") leads to large proofs. Along the way we formalised building blocks such as linear speedup, alphabet reduction, and tape reduction theorems. I will report on tools we developed and progress on refactoring the completed project with unused code identification and higher-order anti-unification, which have so far reduced the 320,000 lines of Isabelle by 10%. Alphabet enlargement (covering linear speedup) and reduction are now in the Archive of Formal Proofs, and the hierarchy results are being prepared for submission.


Microsoft Teams meeting

Join: https://teams.microsoft.com/meet/3268747086619261?p=ApQeTjXxR00iezfU9Y

Meeting ID: 326 874 708 661 926 1

Passcode: dM9QV2Wp

FYI  DReaM stands for Discovery and Reasoning in Mathematics.  It is the name of a research group that Alan Bundy started after arriving at the University of Edinburgh in 1971.  You can read about its history at https://link.springer.com/chapter/10.1007/978-3-030-77879-8_1