一句话：在经典可实现性框架下，首次给出对应于完全选择公理（AC）的显式程序。
经典可实现性为 Curry-Howard 对应提供了一种框架，可将 Zermelo-Fraenkel 集合论中的每个证明关联到一个程序。然而，物理学、概率论和统计学等数学应用通常依赖分析学，即依赖选择（DC）甚至完全选择公理（AC），因此需要为这些公理找到显式程序。此前 DC 已有若干方案，例如称为 bar recursion 的 lambda 项或 LISP 的 quote 指令。本文在经典可实现性框架下构造出完全选择公理的首个程序，从而将 Curry-Howard 对应扩展到使用 AC 的经典数学证明，为从此类证明中提取计算内容提供了基础。摘要未报告实验评估，工作属于理论构造与证明。
The theory of classical realizability is a framework for the Curry-Howard correspondence which enables to associate a program with each proof in Zermelo-Fraenkel set theory. But, almost all the applications of mathematics in physics, probability, statistics, etc. use Analysis i.e. the axiom of dependent choice (DC) or even the (full) axiom of choice (AC). It is therefore important to find explicit programs for these axioms. Various solutions have been found for DC, for instance the lambda-term called "bar recursion" or the instruction "quote" of LISP. We present here the first program for AC.