Lean is becoming increasingly prevalent, as AI demonstrates that formalization is a promising future for mathematics, physics, and beyond.

However, there is a challenge for Lean projects within academia: the success of initiatives like Mathlib and Physlib relies heavily on work that is rarely recognized or rewarded in academic settings. This includes essential tasks such as reviewing, refactoring, onboarding new contributors, and developing foundational areas.

There are models that address this issue - CERN’s 3,000-author papers, for example, show that large-scale collaborative recognition is possible. Regardless of the specific solution the formalization community adopts, I think one thing is clear: we need to accelerate our efforts to find and implement such a solution.

I am fortunate to have a permanent position, but many contributors to projects like Mathlib and Physlib do not. They deserve recognition for their contributions, they deserve to have something they can put on their CVs, and something which others can cite.