LIFT: Library Integration of Formalized Theorems for Reusable Mathematical Knowledge

Automatic formalization produces growing collections of definitions and proofs in Lean, but differences in assumptions and representations impede reuse across projects. We present LIFT, a method for jointly constructing public interfaces and adaptations that recover the original results and prescribed constructions. Existing results are aligned by their full types, common arguments are exposed through general interfaces, and concrete constructions are connected by representation maps. An asynchronous multiple-producer, single-consumer (MPSC) algorithm constructs candidates in parallel and reconciles each change with the current library. Revised candidates can use newly incorporated content; verified releases preserve earlier source recoveries as public interfaces evolve. Integration determines shared statements and adaptations before proof search addresses the remaining obligations. We organize from the public components of 20 previously formalized developments, whose records contain 5,061 accepted integration items. Three checked cases exhibit canonical reuse, general interfaces, and explicit structural data. A promoted normal-cone interface supports a later research proof, while a recorded online revision reuses a newly accepted theorem in its source proof.