Hongfei Fu

Xiaohui Bei, Jiajun Ma, Zhan Jing et al.

Mathematical formalization uses interactive theorem provers to turn informal mathematical statements into machine-checkable artifacts. The success of mathlib, a large collaborative library for Lean, illustrates the potential of this approach. Recent progress in AI-assisted programming and theorem proving is also making large-scale formalization more practical. This paper presents EconCSLib, an early Lean 4 library for computational economics, as both infrastructure and a case study for AI-assisted formalization. The library aims to provide reusable definitions and theorems for game theory, mechanism design, social choice, and related areas. Beyond verified proofs of existing results, the library also aims to host machine-checked open problems and formalization of modern research papers. We discuss the design principles behind the library, the lessons learned from its development, and future directions for AI-assisted formalization in computational economics.

Weiqi Wang, Peisen Yao, Hanrui Zuo et al.

Abstract interpretation provides a principled foundation for constructing sound static analyses through systematic abstraction. A central challenge is synthesizing the best abstract transformers that achieve optimal precision within a given abstract domain. This paper addresses this problem for low-level code modeled with fixed-size bit-vectors. Recent approaches formulate the synthesis task as a multi-objective Optimization Modulo Theories (OMT) problem, but suffer from limited scalability. We introduce Spear, a parallel synthesis framework that exploits a key structural insight: while the bits within each objective must be processed sequentially, the objectives themselves are independent. Spear leverages the independence of inter-objective bits to better parallelize the synthesis. Experimental results on benchmarks across two binary analysis domains show that Spear consistently outperforms state-of-the-art OMT solvers, solving more instances and achieving significantly improved runtimes. To our knowledge, this is the first approach to apply parallelism to accelerate the synthesis of optimal abstract transformers.