Towards the Dream Zone: Better Measurement and Collaboration in Lean

This work explores the application of impact evaluators to reduced-scope Lean formalizations. Lean’s explicit dependency structure, machine-verified correctness, and versioned history make it an ideal setting to test how systematic measurement and evaluation can surface high-impact contributions and improve collaborative progress.