ABSTRACT. In this talk I will discuss two applications of type theory and programming-language techniques in discrete mathematics. The first is a mathematical query language designed for accessing databases of mathematical knowledge. Its queries can be directly read as mathematically meaningful statements, which are type-checked and compiled to SQL. The language can be incorporated into a web frontend to a database, used as a bridge between a proof assistant and a database, and can serve as an interface through which an AI agent accesses the database. The second is a domain-specific type theory for describing discrete finite mathematical structures, whose underlying model is the category of locally finite groupoids. The theory automatically derives the correct notion of isomorphism of structure, and compiles to a low-level language specialized for fast enumeration of combinatorial objects.

ABSTRACT. This article presents an Isabelle/HOL formalisation of simple continued fractions with a focus on executable algorithms. In particular, the two-way correspondence between real numbers and continued fractions is established and various important results are proven, e.g. the connection to best rational approximations.

Additional contributions are: the study of periodic continued fractions, efficient computation of the continued fraction for sqrt(D) where D is a positive non-square integer, the continued fraction expansion of Euler's number, and the connection to Pell's equation.

This machinery is then applied to solve Archimedes' cattle problem, which involves solving an instance of Pell's equation where the solution has over 10^5 decimals.

ABSTRACT. In commutative algebra and algebraic geometry, Hilbert polynomials are an important tool used in the proof of Bézout's Theorem, the construction of Hilbert schemes, and so on. We have used the proof assistant Lean to formalise the Hilbert polynomial of a graded module. Several times, we discovered issues which were not present in the informal proofs but which mattered in the formalisation. As the notions of Hilbert polynomials associated with other algebraic structures rely on the version we have formalised, our project provides a foundation for the future formalisation of them.

ABSTRACT. We present an Isabelle/HOL formalization of the proofs of soundness and consistency of Q₀, a classical higher-order logic equivalent to Church’s Simple Theory of Types. Q₀ provides a very compact and elegant axiomatization of classical type theory with equality and description as its only logical constants.

Our development mechanizes the semantic construction underlying the standard set-theoretic interpretation of Q₀ and formally verifies the soundness of its proof system with respect to this semantics, from which consistency follows as a corollary. To the best of our knowledge, this is the first machine-checked formalization of these central meta-theoretic results for Q₀.

The formalization comprises more than 5000 lines of Isabelle code and required making several implicit arguments in the literature fully explicit, in particular concerning free and bound occurrences, substitutions, etc. The resulting development provides reusable infrastructure for further meta-theoretic investigations of classical higher-order logic within Isabelle/HOL.

ABSTRACT. Partial differential equations (PDEs) are essential for modelling dynamic processes in science and engineering. This project paper presents a framework for the formal analysis in higher-order logic theorem proving of a selected class of linear PDEs with closed-form solutions, including the heat, Laplace, telegrapher’s, and wave equations. We present our existing formalizations of these equations and proofs of the correctness of their analytical solutions for applications such as signal transmission and potential flows using the HOL Light theorem prover. Building on these contributions, we propose a roadmap for extending this framework to additional PDE classes toward a comprehensive foundation for the formal verification of physical systems.