Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre economía titulado Budget imbalance criteria for auctions: A formalized theorem.

Sus autores son Marco B. Caminati, Manfred Kerber y Colin Rowat (de la Univ. de Birmingham).

Su resumen es

We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas.

El trabajo se ha presentado en la 6th Podlasie Conference on Mathematics 2014.

El código de las correspondientes teorías en Isabelle se encuentra aquí.