We must fund intellectual infrastructure for the long term › Funding intellectual infrastructure on the FRO model [013I]

November 17, 2024
Jon Sterling

An interesting and encouraging development is the emergence of the Focused Research Organisation model, which recognises and aims to solve Problem [013K] and Problem [013L]. For example, the most excellent Lean Focused Research Organization describes their mission as follows:

We are excited to share the news of the Lean Focused Research Organization (FRO)! A new nonprofit dedicated to advancing the Formal Mathematics revolution, we aim to tackle the challenges of scalability, usability, and proof automation in the Lean proof assistant. Our 5-year mission is to empower Lean towards self-sustainability. Please check our current roadmap for details. (Lean FRO, Mission)

I think that this is a great development indeed, and it will be good for Lean and therefore good for our community. But I think that the FRO model cannot address Problem [013J]—the inadequate timescale. Even the reference to “self-sustainability” in the Lean FRO mission statement suggests an assumption that there is anything “self-sustaining” whatsoever about the infrastructure that makes scientific and intellectual progress possible.

It is one thing (a very good thing indeed) to solve usability problems and address pain points that prevent institutional and industrial adoption of intellectual tools in the near term. I have every reason to believe that the Lean FRO will be be very successful in this area (and they have made great strides already). An FRO naturally does not aim to solve all problems, and we should certainly not judge them on that unrealistic basis; but we should use the experience to better understand where the gaps are in our current models for the funding and production of intellectual infrastructure.

We must fund intellectual infrastructure for the long term › Funding intellectual infrastructure on the FRO model [013I]

We must fund intellectual infrastructure for the long term [013G]

Funding intellectual infrastructure using research grants [013H]

Problem. Inadequate timescale of research grants [013J]

Problem. Unquantified impact of intellectual infrastructure [013K]

Problem. “implicit” production of intellectual infrastructure [013L]

Funding intellectual infrastructure on the FRO model [013I]

Problems with the bimodal theory/practice cycle [013M]

Unsustainable tool enhancement is a barrier to progress [013N]

A call to action for a sustainable theory/practice spiral [013O]

Acknowledgments [013P]

We must fund intellectual infrastructure for the long term › Problems with the bimodal theory/practice cycle [013M]

Institution. Lean FRO [leanfro]

Problem. We must fund intellectual infrastructure for the long term › Funding intellectual infrastructure using research grants › Inadequate timescale of research grants [013J]

Problem. We must fund intellectual infrastructure for the long term › Funding intellectual infrastructure using research grants › Unquantified impact of intellectual infrastructure [013K]

Problem. We must fund intellectual infrastructure for the long term › Funding intellectual infrastructure using research grants › “implicit” production of intellectual infrastructure [013L]