Applying for NSF Grants for Formalization

Stream: general

[Gregory Wickham]

I will soon (November 14th) be submitting an NSF GRFP proposal in which I propose work on formalizing some of the theory of C*-algebras with Lean. The work I'm proposing is essentially a continuation of the work I'm doing for my undergraduate thesis, to formalize the Gelfand-Naimark theorem.

So, I am asking if anybody here on Zulip has experience getting any kind of NSF (or similar) grants in which they propose formalization work and would be willing to share their proposals or advice with me to help make a specific, compelling proposal?

I'm unsure how to go about proposing a convincingly specific plan when it is very difficult to estimate how long a formalization project might take and to figure out what results might be most useful to formalize.

[Jeremy Avigad]

@Gregory Wickham Formalized mathematics is a new industry, especially in the US, and you may have a hard time finding a good model for a GRFP proposal. However, in recent years the NSF DMS has made it clear that they are interested -- see e.g. the AIMing program and the new NSF institute ICARM. A couple of years ago there was even an explicit call for REUs that incorporated formal methods and formalization.

In short, I expect the proposal you describe will be new to them, but they will be interested. It may find its way to reviewers who know something about formalization, but it may instead go to analysts. Whatever you do, try to write something that will be interesting and accessible to both audiences. It will help to describe what is currently in the library, what you think should be done next, and how you plan to go about doing it. The proposal should convince reviewers that formalizing the theory of C* algebras is a good thing to do and that you are capable of doing it. It's o.k. to be tentative; you can characterize some components of the proposal as straightforward and others are more ambitious.

[Filippo A. E. Nuccio]

Gregory Wickham said:

I will soon (November 14th) be submitting an NSF GRFP proposal in which I propose work on formalizing some of the theory of C*-algebras with Lean. The work I'm proposing is essentially a continuation of the work I'm doing for my undergraduate thesis, to formalize the Gelfand-Naimark theorem.

So, I am asking if anybody here on Zulip has experience getting any kind of NSF (or similar) grants in which they propose formalization work and would be willing to share their proposals or advice with me to help make a specific, compelling proposal?

I'm unsure how to go about proposing a convincingly specific plan when it is very difficult to estimate how long a formalization project might take and to figure out what results might be most useful to formalize.

With @Riccardo Brasca we submitted a succesful grant aiming at formalizing some number theory/arithmetic to the French equivalent of the NSF and we can share details in DM.

[Gregory Wickham]

Jeremy Avigad said:

Whatever you do, try to write something that will be interesting and accessible to both audiences. It will help to describe what is currently in the library, what you think should be done next, and how you plan to go about doing it. The proposal should convince reviewers that formalizing the theory of C* algebras is a good thing to do and that you are capable of doing it. It's o.k. to be tentative; you can characterize some components of the proposal as straightforward and others are more ambitious.

Thank you for this advice and for pointing me to examples of the NSF funding projects involving formalization!

[Gregory Wickham]

Filippo A. E. Nuccio said:
With @Riccardo Brasca we submitted a succesful grant aiming at formalizing some number theory/arithmetic to the French equivalent of the NSF and we can share details in DM.

Thank you so much! I'll DM you now.