Events and news relevant to the Laboratory for Foundations of Computer Science

[Paul Jackson <Paul.Jackson@ed.ac.uk>]

A reminder about the talk at 2pm today in IF MF2 and on Teams:

From: Paul Jackson <Paul.Jackson@ed.ac.uk>
Date: Monday, 26 October 2026 at 17:58
To: aiai-members@inf.ed.ac.uk <aiai-members@inf.ed.ac.uk>; LFCS Interest <lfcs-interest@mlist.is.ed.ac.uk>; 'inf-ianc-talks@mlist.is.ed.ac.uk' <inf-ianc-talks@mlist.is.ed.ac.uk>; inf-dreamers@mlist.is.ed.ac.uk <inf-dreamers@mlist.is.ed.ac.uk>
Cc: Andras.Salamon@st-andrews.ac.uk <Andras.Salamon@st-andrews.ac.uk>; Alan Bundy <A.Bundy@ed.ac.uk>
Subject: Joint AIAI-DReaM seminar: Mon 2 Nov 2pm - Andras Salamon on formalising complexity theory

Hi,

on Monday 2^nd November 2-3pm there will be a joint AIAI & DReaM group seminar in Informatics Forum MF2 and online.

(If you are unfamiliar with the DReaM group, see the end of this announcement)

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

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.