Seminars

Home Schools Computational Sciences Seminars

TITLE: Transforming classical mathematics in type theory (e.g. Lean) into oracle computation

ABSTRACT: In the practice of formalizing classical mathematics, classical principles such as the axiom of choice or the law of excluded middle are typically assumed as global functions realizing them. For instance, the Mathlib library of the Lean theorem prover assumes a single function that, given any nonempty type, chooses an element of it. This way of assuming classical principles, however, makes classical results hard to reuse in a constructive (or computational) setting, where it is inconsistent to assume a functional realizer that works uniformly for all inputs. Instead, we consider oracle computation as a controlled and consistent way of assuming classical principles inside a constructive type theory: rather than having a function, we restrict the classical principles to be accessed only by querying an oracle. This way, classical results can even be refined into computations whenever the oracle queries can be resolved. In this talk, I present progress from our ongoing work with Andrej Bauer and Danel Ahman on transforming classical results in type theory into oracle computations. This extends my talk at Continuity, Computability, Constructivity --- From Logic to Algorithms (CCC 2026, Kyoto), now aimed at a broader audience not necessarily familiar with type theory. This talk may also interest anyone curious about forcing and sheaf semantics in type theory.