Uploaded February 2026 | Updated September 2026, 2 weeks ago
Topos Institute Colloquium, 19th of February 2026.
———
Advances in autoformalization suggest the possibility of automatic translation between natural language mathematics and formal verification programming languages. We'll chart this recent progress in mathematics. We will consider implications for mathematics, and science more broadly.
Topos Institute Colloquium, 19th of February 2026.
———
Advances in autoformalization suggest the possibility of automatic translation between natural language mathematics and formal verification programming languages. We'll chart this recent progress in mathematics. We will consider implications for mathematics, and science more broadly.
![[Oxford Seminar] Greg Neustroev | The Treachery of Certificates: Ceci n’est pas une supermartingale](https://i.ytimg.com/vi/ZO7KmOXGX98/mqdefault.jpg "[Oxford Seminar] Greg Neustroev | The Treachery of Certificates: Ceci n’est pas une supermartingale
Oxford Seminar, June 25 2026
You can view the listing for this talk online at https://topos.institute/events/oxford-seminar/talks/2026-06-25_neustroev_treachery.html
Speaker: Greg Neustroev
Full Title: The Treachery of Certificates: Ceci n’est pas une supermartingale
Abstract: To prove that a stochastic system exhibits a desired behavior with high probability (for example, that it reaches a target while avoiding danger) it often suffices to produce a single function on its states satisfying a few pointwise inequalities: a supermartingale certificate. Finding such a function is the hard part; checking one is easy, which is why neural networks, as flexible function-searchers, have become a natural tool for the job.
But a certificate is a static object — a function you can write down — while the object that actually carries the proof is a stochastic process: its dynamic interpretation as it rides the systems randomness. These are not the same thing, and the passage between them is not canonical: one function can induce many supermartingales, depending on how we stop, shift, or time-compensate it. Well build both objects from scratch, make the construction explicit, and see why conflating them — a common slip, even among practitioners — is exactly where soundness is won or lost.")
![[Berkeley Seminar] Benjamin Brast-McKie | Programmatic Semantics](https://i.ytimg.com/vi/ZqTpdJKHT_4/mqdefault.jpg "[Berkeley Seminar] Benjamin Brast-McKie | Programmatic Semantics
Title: Programmatic Semantics
Abstract: This talk presents a programmatic methodology which uses the model-checker software that I developed to rapidly prototype semantic theories.
I will begin by presenting a standard methodology in philosophical logic to highlight a number of shortcomings which motivate the programmatic methodology. I will then introduce the model-checker which draws on the SMT solver Z3 to rule out finite countermodels of a user specified size, providing evidence that a logical consequences has no countermodels if in fact there are none. Implementing a programmatic semantics with the model-checker extends the standard methodology by easing the process of exploring and prototyping novel semantic theories.
In addition to facilitating the study of complex semantic theories, the model-checker provides resources for uploading semantic theories to the TheoryLib to facilitate collaboration. Programmatic semantic theories are also modular, making them easy to combine and compare, allowing users to survey the interactions in languages with many operators. Moreover, the computability of a semantic theory provides an objective measure that may be weighed alongside other theoretical virtues.
Although the model-checker is a general purpose utility for working in semantics, applications in hyperintensional semantics are particularly natural given the increased complexity of these semantic systems. Rather than a deficiency, I will characterize well-motivated forms of theoretical complexity as a sign of the maturity of semantics as a discipline. It is in support of both the future development and accessibility of semantics that the model-checker aims to make a contribution. The talk will conclude with a brief demonstration to make the workflow concrete.
Date: 2025-06-17
https://topos.institute/events/berkeley-seminar/")
![[Berkeley Seminar] Michael Arntzenius | UC Berkeley](https://i.ytimg.com/vi/_A9qrqL2D28/mqdefault.jpg "[Berkeley Seminar] Michael Arntzenius | UC Berkeley
Title: A type system for finitely supported functions via pointed sets, Part 2
ABSTRACT:
Finite maps, in the form of dictionaries, associative arrays, or tables, are a key data type in most language’s standard libraries, but constructing and manipulating them is generally very explicit and loopful. In this talk I’ll demonstrate work in progress on a type system that can guarantee that functions written directly as lambda-expressions are finitely supported, and therefore can be represented as tables. This yields a higher-level, more declarative syntax, similar to logic programming languages or database query languages.
The semantics of my language live in Set, the category of pointed sets and point-preserving maps. In order to define the support of a function f: A → B, one needs a point nil ∈ B; then support f = {x ∈ A : f x ≠ nil}. In fact, finitely supported maps form a graded monad on Set; they are graded by their domain A. To fully flesh out the semantics and type system, I also need the free/forgetful adjunction between Set and Set*.
Unfortunately the typing rules get quite complex. I’d like to know if there’s a simpler way to accomplish the same goals, or a simpler or more general framework for presenting the type system itself.
Paper preprint for the interested: https://www.rntz.net/files/finite-functional-programming.pdf
Date: April 7, 2026")
![[Oxford Seminar] Q Le | Free PLTL Algebras and A Coalgebraic LTL Extension of Hyperdoctrines](https://i.ytimg.com/vi/_IHFAxbHYfM/mqdefault.jpg "[Oxford Seminar] Q Le | Free PLTL Algebras and A Coalgebraic LTL Extension of Hyperdoctrines
Oxford Seminar, 18th of September 2025
Abstract: In this seminar, I describe the work I had done over the summer of 2025 at the Topos Institute with José Vitor Paiva Miranda de Siqueira. Inspired by the free Boolean/Heyting algebra of a given set, we develop a free-forgetful adjunction between posets and PLTL temporal algebras, where PLTL denotes propositional linear temporal logic. We provide a description of their induced Eilenberg-Moore categories. We describe how this could be used to temporalise systems and logics through hyperdoctrines and connect this to the stream comonad. We end with future research directions, connecting this topic with the cofree comonad of polynomial functors and temporalising doxastic logic.")
![[DOTS Lectures] 16. Monadicity of double operad algebras](https://i.ytimg.com/vi/_suTwV_UQtc/mqdefault.jpg "[DOTS Lectures] 16. Monadicity of double operad algebras
Part of a lecture series on the Double Operadic Theory of Systems (DOTS) presented by David Jaz Myers.
Some material from these lectures can be found in Davids book on categorical systems theory:
https://www.davidjaz.com/Papers/DynamicalBook.pdf")
![[Berkeley Seminar] Victoria Vollmer | From Graded Foundations to the Foundations of Grading](https://i.ytimg.com/vi/_wLFg3YNfsE/mqdefault.jpg "[Berkeley Seminar] Victoria Vollmer | From Graded Foundations to the Foundations of Grading
Title: From Graded Foundations to the Foundations of Grading
Abstract: In recent decades, monads have come to be an indispensable tool in programming language theory and practice. Graded monads, which generalise monads by allowing the operations of a monad to be ‘stratified’ by a monoid, are a relatively recent innovation which provides the same utility as monads but utilises the monoid structure to provide more fine-grained control. As the use of graded monads rises so does the need to understand them formally. This work examines graded monads as lax 2-functors, to build up to a 2-category of graded monads. This provides concrete definitions of morphisms between graded monads, graded monad distributive laws, and composition of graded monads. We then demonstrate the utility of the 2-category of graded monads by providing the free graded monad construction. Further we show how using the notion of internal graded monad, we can define graded multicategories–which can be used to model graded base logics–as an extension of Leinster’s generalized multicategories.
Date: May 14, 2026")
![[Oxford Seminar] Tim Hosgood | Open translations in mathematics](https://i.ytimg.com/vi/ac7laU1WH7o/mqdefault.jpg "[Oxford Seminar] Tim Hosgood | Open translations in mathematics
Oxford Seminar, 20th of March 2025
Translation, in full generality, is a nuanced and complex art form that requires serious expertise and a holistic approach. So how can we as mathematicians hope to solve the problem of translation in our domain? Furthermore, can we do so without making access to academia even harder for non-native English speakers or hurrying a domain collapse of non-English languages? I believe that the answer to both of these questions can only possibly be yes if we approach translation as a community-driven activity. In this talk, I will speak about my experiences in working on large translation projects with an open-source approach — the technology and methodology that was helpful for doing so, as well as some of the difficulties — and describe the sorts of resources that I believe would have been helpful. Hopefully this can form a starting point for community thought on the types of projects that we could focus on in the future. (This talk is a repeat of a talk given recently at the Isaac Newton Institute).")
![[Berkeley Seminar] Michael Arntzenius (Topos Institute) | A perfect join algorithm?](https://i.ytimg.com/vi/ambisA2jegA/mqdefault.jpg "[Berkeley Seminar] Michael Arntzenius (Topos Institute) | A perfect join algorithm?
Title: A perfect join algorithm? Answering queries in optimal time: Yannakakis’ algorithm
Abstract: If we have a query over some database, how fast can we find all answers for it? If we don’t assume any additional structure (such as indexes on the database), the best possible time is O(IN + OUT): that is, the size of the input (the database) plus the size of the output (the matches for the query). Since we didn’t assume anything about the structure the database is in, any part of it could be relevant, so we have to read the entire database; and by definition we have to write the entire output. Is this achievable? It is, for a particular class of queries: the α-acyclic queries. In this talk I’ll explain how to view queries (and databases) as labelled hypergraphs, define α-acyclicity, and show why and how it allows us to answer queries in linear time using Yannakakis’ algorithm (YA). If I have time, I may: - explain more practical variants on YA such as TreeTrackerJoin - explain the fractional edge cover bound on a query/hypergraph, and how to achieve it using worst-case optimal joins, which handle cyclic queries. - (unlikely) explain further generalizations such as hypertree decompositions of queries.
Date: Aug 4, 2026")
