arguments for why formalization should "count" as research?

Stream: general

[Alex Kontorovich]

I'm sure others have had this experience, so I wanted to crowdsource some ideas: I pinged my NSF program director about a grant we wanted to put in to train our undergrads through postdocs in Lean. The director replied that it seemed like a nice idea, but it should have a substantial "research" component. Of course the underlying presumption is that formalizing math isn't real research math. (Fair enough, we're not really producing "new" theorems... yet.) I was going to craft some long discussion about why this should still count as research, because we're learning so much about basic mathematics in the process of formalization, etc etc. But maybe others have had similar experiences and found stronger arguments?... Thanks!

[Kevin Buzzard]

The computer science people are well aware that what we are doing with mathlib is research: things like IsScalarTower, handling semilinear maps, managing typeclass inference etc etc are new results in CS which had to be solved because mathematicians were pushing to build a maths library. But if they really mean research math then I guess you point them to things like Commelin's simplification of the Clausen-Scholze argument, which came out of a formalisation. David Ang and Junyan Xu gave what is as far as I know a new proof of associativity of the group law on an elliptic curve over an arbitrary field which came from trying to understand a reasonable path to a formalisation of the result. But I agree, it's difficult to find evidence right now. I think a more plausible argument is that funding bodies should step back and say "OK we've been funding new research math for ages and we know what that does, but actually what will this area achieve long term? Maybe it will achieve completely new things which we haven't even thought about". I would say that working in this area is far likely to achieve completely new things which we haven't even thought about than just proving more theorems; we know exactly what it looks like if you fund an area and get a bunch more theorems proved -- it just becomes a bigger area. We don't really know what happens if you build a gigantic thing like mathlib.

[Matthew Ballard]

What will be effective heavily depends on the solicitation you are targeting I think

[Matthew Ballard]

What you describe sounds like reads as workforce training regardless of Lean's involvement.

[Matthew Ballard]

Perhaps answering a more question will help: What new things do you expect to come from this proposal beyond improved facility with Lean for students through postdocs?

[James B. Wilson]

I'm what some people call a "Computational Algebraist" and have written various large and small packages for Magma, GAP, and as well as special purpose programs. But I also have to apply for grants and publish papers in math journals. So in that role I have long had such issues. As. rule of thumb, I feel that if you can't see where you would publish such a result then you probably cannot expect a funding agency to have a program that will fund it. So with that in mind here is some general comparable situations and how they lead to publishing and funding.

[James B. Wilson]

There are few outlets from places like SIAM journals where you can publish what might be crudely described as a "manual" to a critical package of mathematical software. But that tends to narrowly apply to specific contexts (multigrid, PDE solvers, various core Linear Algebra things). And indeed you can find many NSF funded grants on those algorithms, under applied Math or under various types of computer science. But if for example you make a package in Sage to compute with elliptic curves and what it does is re-route the calls to Macaulley or Singular or GAP then realistically you will struggle to get that work accepted for a publication and funding will likewise be hindered.

[James B. Wilson]

So in such a case you often are lead to two choices:

• Prove a theorem about how the algorithm works: does it halt and no one before you even knew a solution existed? Or does a brute-force algorithm exist but yours will be more efficient, say in polynomial time or better?
• Compute something with it. Does your work let you now classify all the widgets of genus 7? Or disprove a conjecture of Erdos?

[James B. Wilson]

Results like that can be published and are good motives for funding, provided the story is authentic.

[James B. Wilson]

Now pivoting to something like MathLib, if I were reviewing proposals that seemed to suggest the goal was some sort of "Noah's Arc for Theorems" I'd be a bit dismissive myself. After all I could play devils advocate and say large language models will soon be able to just read math books as written and thus read the proofs without the need for the middle man (or woman). ---I don't believe that just saying the obvious objection in hyperbolic terms.

[James B. Wilson]

So instead imagine your goal is to explore one of two possible avenues.

• Does the type of formalization reveal a new strategy in proof theory? Does it need a special form of type theory or lambda calculs?
• Does it let you resolve an application? For example, will building the theorems in topology let you make a proveable model of a modal logic that could be used in applications control theory?

[James B. Wilson]

At first it may seem artificial to think of a motive like that when perhaps what you really want is just to get to formalize something you feel could be better understood, but honestly I have found a constraint like one of these really helps me focus on a purpose and give me clear goals. And that it fits with the usual publishing/funding world view is a necessary bonus.

[James B. Wilson]

In summary think about whether your plan will encounter new ways of proving things or if it can be put to use once made to offer a computational foundation for some applied goals. That's not the sum total of ways to get things funded but it has been a useful strategy in my discipline.