I'm curious as to whether you think the status of your "Central Dogma" has changed in the light of recent developments as is perhaps suggested by this NSF solicitation.
When asserting that "there are far more worthy proposals in more conventional areas than the number already being funded", is this primarily because the Central Dogma (say - an effective, wholesale formalization of mathematics) remains a chimera or is it because, say post-GenAI/Lean etc., such mechanization now seems inevitable but with the claimed downsides/risks? In other words, is this proposal less worthy than those in conventional areas because the Central Dogma is true or because it is false?
The syntax of that quotation may be misleading. I didn't mean to say that the more conventional proposals are necessarily more worthy than those that will be funded by this new solicitation, but rather that the NSF budget in mathematics was already strained before the new call came out, and insufficient to fund all the proposals that deserve to be funded. I base this judgment on my experience on an NSF panel. This is completely independent of my judgment of the status of the Central Dogma.
I can imagine that there may be pressure on the Division of Mathematical Sciences to expand the new program at the expense of core areas of mathematics; but I can also imagine that the NSF may increase funding overall and that support for non-mechanized mathematics may remain intact or may even increase. It is likely to be hard to get a sense of this evolution, because so many factors determine NSF's priorities.
The picture of "the differential equation with less than 3 elephants" calls to mind Jim Gleick's lovely phrase in Chaos that one could describe mammals as "non-elephant animals".
I'm curious as to whether you think the status of your "Central Dogma" has changed in the light of recent developments as is perhaps suggested by this NSF solicitation.
When asserting that "there are far more worthy proposals in more conventional areas than the number already being funded", is this primarily because the Central Dogma (say - an effective, wholesale formalization of mathematics) remains a chimera or is it because, say post-GenAI/Lean etc., such mechanization now seems inevitable but with the claimed downsides/risks? In other words, is this proposal less worthy than those in conventional areas because the Central Dogma is true or because it is false?
The syntax of that quotation may be misleading. I didn't mean to say that the more conventional proposals are necessarily more worthy than those that will be funded by this new solicitation, but rather that the NSF budget in mathematics was already strained before the new call came out, and insufficient to fund all the proposals that deserve to be funded. I base this judgment on my experience on an NSF panel. This is completely independent of my judgment of the status of the Central Dogma.
I can imagine that there may be pressure on the Division of Mathematical Sciences to expand the new program at the expense of core areas of mathematics; but I can also imagine that the NSF may increase funding overall and that support for non-mechanized mathematics may remain intact or may even increase. It is likely to be hard to get a sense of this evolution, because so many factors determine NSF's priorities.
The picture of "the differential equation with less than 3 elephants" calls to mind Jim Gleick's lovely phrase in Chaos that one could describe mammals as "non-elephant animals".