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 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 mathematics into oracle computation inside a constructive type theory. This talk extends my CCC 2026 (Kyoto) talk.