Terence Tao on Nostr: Any complex project tends to have both explicitly stated and implicitly unstated ...

Any complex project tends to have both explicitly stated and implicitly unstated target goals. For instance, a Lean formalization project may have as its explicit goal the task of obtaining a formal proof of some mathematical claim X; but there are often unstated goals, such as also formalizing key subclaims and definitions X_1, X_2, ... to X in a fashion that would be suitable for upstreaming to the Mathlib library; learning how to use various collaboration tools and distribute tasks; organically discovering insights to the finer structure of the proof of X that might not be emphasized in previous informal proofs; giving real-world training and experience to novice formalizers; and more generally building a community of humans expert in the art of formalization.

In the past, it has generally not been necessary to state these implicit goals because of a strong empirical correlation between the achievement of these goals and the achievement of the explicit goals. In the example of the formalization project, pretty much any human-centric effort to accomplish the explicit goal will end up naturally also achieving most of the implicit goals stated above. So the explicit goal effectively becomes a viable proxy for the broader range of actual goals. (1/2)