Rebuttal


**** 1.1 ****

All four key objectives carry far-reaching innovations and introduce new techniques:

1. The planned extensions to Aesop (forward reasoning, arithmetic, induction) will bring a uniquely strong white-box automation tactic with no counterpart in any proof assistant based on dependent type theory.

2. The Lean Hammer will be the first well-tuned hammer for dependent type theory. Moreover, it will be the first hammer to integrate the new generation of efficient higher-order provers.

3. Today, proof assistants are strong on proofs but weak on computation and largely lack the convenience of computer algebra systems. The proposed research will bring verified computer-algebra-style reasoning to the vast field of effectively resolving Diophantine equations and beyond. A particularly rewarding aspect of this task concerns the generation of proof certificates.

4. Diophantine equations form a central topic in number theory. A coherent formal library for Diophantine equations will be entirely new.

It is true that Isabelle already provides some of the automation we want to add to Lean. Indeed, some of Isabelle's automation was developed by the co-PI. However, we now propose to design the automation for a much richer logic: Lean's dependent type theory. This poses many new challenges. Mathematicians are using Lean precisely because they determined that to develop a large, coherent library of formal mathematics, they need dependent types.

Our plan is to build on existing proof assistants and tools. This is a strength of the project, since it helps minimize the amount of engineering, allowing us to focus on the deeper scientific questions, such as how to encode dependent type theory in higher-order logic to exploit automatic provers. We are aware of Rothgang et al.'s translation cited by referent 2, which indeed does not look very promising. We plan to base our translation on the ideas of Cruanes and Blanchette, "Extending Nunchaku to Dependent Type Theory" (2016). The main advantage of this translation is that it locally encodes any dependent type feature, avoiding clutter. We expect that it can be extended and that (nondependently typed) higher-order provers can actually provide strong automation for dependently typed theory.

The computer science parts of the project are as ambitious as the mathematics parts. The main challenge regarding Aesop concerns the integration of various techniques under one roof. For the hammer, the difficulties are connected to the high expressiveness of dependent type theory. These two tools will obviously be very useful to achieve the objectives of task 4. Referent 3 points out that other tools might be useful. But in the absence of tools, users can still make progress, albeit more slowly. We focus on the two tools we believe will make the biggest difference.

Even though it contains, as noted by referent 1, some computer science aspects, task 3 is primarily a mathematical undertaking. The development of proof certificates and number-theoretical algorithms are firmly rooted in mathematics.

The choice of Lean 4 is motivated by the desire to reach mathematicians. Lean boasts a large, coherent, community-driven library of mathematics developed by mathematicians. This library, and especially the parts about advanced number theory, will be crucial for our project. But regardless of the vehicle, the goal is to advance science. Despite the proof assistant community's fragmentation, substantial advances in one system usually translate into advances in others. Many tools have been ported, even across systems with different logical foundations. As always, the real progress is conceptual, not technical.


**** 1.2 ****

The development of tools such as Aesop and the Lean Hammer greatly benefits from case studies. Referent 1 correctly observes that other case studies could have been considered instead. However, the unique blend of computation and proofs in the number theory parts of the project makes it an ideal playground for our tools. Moreover, the PI and co-PI already have experience collaborating, supervising two PhD students together, maximizing the chances that this new collaboration will be a success.

To attain key objective 3, as mentioned in our rebuttal to 1.1, task 3 is best performed by a mathematician.


**** 1.3 ****

n/a


**** 2.1 ****

Referent 1 opines that they do not feel that "showing the society that mathematical research is very much alive today" has significant societal impact. Referent 3 has the opposite opinion. So do we. (Also see the first paragraph of referent 2's comment at 2.3.)

We agree with referent 1 that adoption of formal verification in the industry is a long-term goal that will likely not be met within the time frame of the project.

As observed by referent 1, a "very long term" impact is the use of proof assistants to support the daily development of new mathematics. Indeed, it is the big dream shared by many researchers in the interactive theorem proving community. Part of this dream, as remarked by referent 3, is that the mathematical review process will be more rigorous and effective. Our proposal, if funded, could contribute to this dream.

Referent 3 points out the importance of potential applications to cryptographic software. We agree about this, as well as other long-term societal impacts; however, this is not the focus of our proposed research.


**** 2.2 ****

We are not proposing to formally verify an existing computer algebra system. Instead, we plan to certify external output data inside Lean. As long as the output format remains the same, there is no need to "re-verify every update". Certification means that we can use computer algebra algorithms to help develop formally verified proofs. It would also offer, to mathematicians who have worries about the trustworthiness of computer algebra systems, formally verified tools.

Concerning the focus on Lean 4, we largely agree with referent 3 that our real focus should be on the science and not on the system. We have experience with other proof assistants and collaborators using them. We will indeed pay attention to this aspect and make sure our research will have an impact beyond the Lean community. See also the last paragraph of our rebuttal to 1.1.


**** 2.3 ****

We agree with referent 2 that much more work needs to be invested before proof assistants are widely adopted by industry. This is indeed outside the scope of this proposal.

Concerning referent 3's comment, see our rebuttal to 2.1.


**** 3 ****

We are pleased to read that all three referents see many strengths in our proposal. Most of the points they raise as weaknesses were already addressed above. For completeness, we address all perceived weaknesses below.

Concerning innovation and incrementality, see the beginning of our rebuttal to 1.1.

Concerning the collaboration, see our rebuttal to 1.2.

Concerning the difficulty of hiring a postdoc with knowledge of both proof assistants and Diophantine equations, we point to our track record; see section A.2.5 of the proposal. We enjoy a large network to draw candidates from. If we nevertheless should fail at finding a suitable candidate with expertise in both aspects, we will (as we have occasionally done in the past) settle for a candidate who masters the mathematics and who is eager to learn proof assistants. Our experience makes us very confident that hiring will not be a concern.

Concerning the feasibility of higher-order provers for solving dependently typed proof obligations, see the fourth-to-last paragraph of our rebuttal to 1.1.

Concerning the fact that tasks 1 and 2 may not be enough to achieve task 4, see the third-to-last paragraph of our rebuttal to 1.1.

Concerning the choice of Lean and the impact beyond Lean, see the last paragraph of our rebuttal to 1.1 and the last paragraph of our rebuttal to 2.2.

In conclusion, the formalization of mathematics has a long history, especially in the Netherlands, starting with the pioneering work of Nicolaas De Bruijn. But only in the past few years have research mathematicians started to widely adopt proof assistants, with top mathematicians such as Peter Scholze and Terence Tao engaging with the field. Proof assistants are evolving fast and promising to become indispensable tools for future mathematicians. This project is very timely and will make a real difference. In addition to the PI and co-PI, it will involve two hired staff and several collaborators (e.g. Assia Mahboubi, Jannis Limperg, Gabriel Ebner, Alex J. Best; see A.2.4 of the proposal). Through workshops, publications, and our scientific network, we also expect the project to gain high visibility and attract further collaborators.
