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 so that they may be accessed only by querying an oracle. That is, for a type X, we consider instead an inductive type O(X) whose constructors either embed an element of X or build a term of O(X) from an answer to a query, for example, an element of a nonempty type. 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 project with Andrej Bauer (University of Ljubljana, Slovenia) and Danel Ahman (University of Tartu, Estonia) on transforming classical results in type theory into oracle computations. Previous work, including (D. Ahman and A. Bauer 2026) treated the case where the classical principle is propositional, that is, where the type of answers to each oracle query is a subsingleton, which includes the law of excluded middle. However, it did not extend well to the nonpropositional case, where a single query may have more than one possible answer, as in Lean's formulation of the axiom of choice. The focus of our work is to extend the theory to the nonpropositional case by lifting the oracles into a forcing setting where the nonpropositional oracle becomes propositional. We also present a prototype Lean metaprogram implementing the transformation on a small fragment of Lean's type theory.

This talk practices my invited talk at CCA 2026(Trier).

​Sewon Park is a postdoctoral researcher at the Institute of Mathematics, Physics and Mechanics (IMFM) in Ljubljana, Slovenia, hosted by Prof. Andrej Bauer. He received his PhD in Computer Science from KAIST in 2021 under Prof. Martin Ziegler, and previously held postdoctoral positions at Kyoto University, including a JSPS Postdoctoral Fellowship at RIMS. His research spans syntax and semantics of type theory, computable analysis, and the formalization of constructive, computable, and classical mathematics in dependent type theory, together with their implementation in proof assistants such as Rocq and Lean.​