"Issues" and (selected) "Positive remarks"

****************
***  Issues  ***
****************

***** 1.1
- Ref 1
[a] B) The proposal is not particularly innovative, in the sense that it will exploit and enhance tools and techniques that have already proved themselves effective in other contexts. On the other hand

D)
One potential weakness of the proposal consists in the first subtask and objective assigned to mathematicians, the one about exploiting external computer algebra systems to obtain trusted computations inside Lean. While the task can require a significant level of understanding of the math involved, it seems to me more adequate for a team with strong computer science background. I suppose 

The computer science-related tasks are not too ambitious and they are likely to yield good enough results in the project timeframe. I would honestly be surprised if these results would not been delivered. On the other hand the mathematician-related tasks seem overly-ambitious to me, even with a dedicated post-doc, and I would expect the final outcome to cover only a subset of the expected mathematical results. Nevertheless

- Ref 2
On the other hand, it is not entirely clear to me what degree of novelty is inherent in B.1. Arguably, and also as referred to by the proposal, there are strong means of automation available in Isabelle/HOL, including its Sledgehammer system (hammer-style proof automation) and various automated tactics (white-box proof automation)

Recent work [1] looks at a related task and concludes that the automation provided by a translation to higher-order logic is not necessarily effective.

However, it is not entirely clear to me to what extent C.2 addresses basic research aspects, or whether it primarily consists of (challenging) engineering work (see B above).

The basic premise of the proposal, i.e., the usage of Lean 4, is not clearly motivated. Why is Lean 4 chosen out of the range of possible proof assistants? Of course, it is a prominent system; but others are well-engineered, too (such as Isabelle/HOL with its mature automation mechanisms).

- Ref 3

In my opinion the approach might not be up the ambition of the authors, but if only, say, 50% of their objectives were to succeed, the project would still be worth it, so this does not hinder my appreciation for the proposal. My main concern is that tools like aesop and hammers are only two of numerous ways of achieving automation in dependent type theoretic proof assistants, and while their improvement (tasks 1 and 2) is most certainly a desirable line of research, they might not be the only two keys (even combined with task 3) for the success of task 4


***** 1.2
- Ref 1
Moreover, the majority of the work done at the Munich site by computer scientists would benefit equally well from other partners that formalize completely different parts of mathematical knowledge.

As I wrote before, the latter statement is maybe more dubious for Key Objective 3 (performed by mathematicians, but requiring good computer science background), but the potentially missing expertise can be filled in by other local collaborations of the applicant. 

- Ref 2
- Ref 3

***** 1.3
n/a

***** 2.1
- Ref 1
I do not have the feeling that "showing the society that mathematical research is very much alive today" has significant societal impact. The other impacts listened have to do with better proof automation that could benefit adoption of formal verification in the industry. However, this is not an impact expted in a significant way in the timeframe of the project. Moreover, improving automation is only related to one half of the project objectives.
On the other hand, I think that the applicants could have pointed out a potential, but extremely rewarding, very long term societal impact: ...


- Ref 2
- Ref 3
they do not stress out enough in the final section A.3 that there might also be a strong impact in the review process of scientific contributions

Because of the latter point and because of the importance of the application to cryptographic software, I would like to stress out that to me, the scientific and societal impact are of comparable focus, even though the authors downplayed (in my opinion) the societal impact.

***** 2.2
- Ref 1
B) The applicants do not discuss any impact on science in general

- Ref 2
but I'm not sure whether it will indeed increase the perceived reliability of computer algebra systems -- the connection between formally verified procedures, implementations, and outputs of such systems might not be apparent to mathematicians that are not engaged in such computational topics. Also, computer algebra systems are often updated, and it seems infeasible to re-verify every update. Still, some of the anticipated aspects will certainly occur in the Lean 4 community (who use the tool anyway).


- Ref 3
I would like to point out a potential shortcoming of the proposal as it is today. The proposal is mostly geared towards a specific software called Lean 4. ...

***** 2.3
- Ref 1

- Ref 2
 it is claimed that the development of tools like Lean 4 fosters the usage of such tools in industry. While I generally agree, I think much more work needs to be invested before this becomes feasible (which is outside the scope of this project proposal).

- Ref 3
Not addressed by the applicants, even though, as I noted above, I believe it should have been.

***** 3
- Ref 1

the proposal is mostly incremental: it does not introduce new lines of research, nor it is aimed at developing new techniques

 the two teams have their own set of objectives; developing both at once in a single project with frequent interaction will speed up both developments; however the objectives could be achieved less effectively even if developed independently: collaboration in this case is useful, but not necessary

the project assumes to be able to hire a post-doc with previous expertise on..

- Ref 2

Insufficient explanation of the choice of Lean 4 as proof assistant

Innovativeness unclear for the described automation methods

No evidence for the feasibility of higher-order theorem provers for solving dependently-typed proof obligations

- Ref 3

Tasks 1 and 2 may not be enough to achieve task 4 as envisioned.

The research must have impact beyond a specific software such as Lean 4.

***** 3 (again)

Innovation

- Innovativeness unclear for the described automation methods

- the proposal is mostly incremental: it does not introduce new lines of
  research, nor it is aimed at developing new techniques


Collaboration

- the two teams have their own set of objectives; developing both at once in
  a single project with frequent interaction will speed up both developments;
  however the objectives could be achieved less effectively even if developed
  independently: collaboration in this case is useful, but not necessary


Hiring

- the project assumes to be able to hire a post-doc with previous expertise
  on interactive theorem proving and deep expertise on diophantine equations;
  the PI is likely to have the best contacts to find such candidates. The pool
  to pick from, however, is quite small, and if hiring fails or the candidate
  is not expert in both topics, then the likelihood of reaching all goals is
  decreased


HOL

- No evidence for the feasibility of higher-order theorem provers for solving
  dependently-typed proof obligations


Tools for task 4

- Tasks 1 and 2 may not be enough to achieve task 4 as envisioned.


Lean

- Insufficient explanation of the choice of Lean 4 as proof assistant

- The research must have impact beyond a specific software such as Lean 4.


**************************
***  Positive remarks  ***
**************************

------
1.1 Ref 1:
Recently the Lean prover seems to be completely changing the picture: it has managed to attract an ever growing community of mathematicians that are building a huge, connected library staying close to the usual mathematical foundation and already close to cover all of the standard topics taught in a math curricula and some advanced material as well.

1.1 Ref 2:
B.2 is clearly novel and innovative, as there are few to none formalizations of Diophantine equations available -- even when considering different proof assistants such as Isabelle/HOL, Coq, Lean and Mizar. Even more, the verification of Diophantine computations provides important insights and increased reliability for computer algebra systems, and an important interface between computations and formalized properties.

1.1 Ref 3:
The four objectives are indeed innovative, by promising nontrivial extensions to solid, albeit recent, previous work, some of which were done by the applicants and their collaborators

1.2 Ref 2:
This project would hardly be possible without one of the two collaborating researchers: The main applicant provides expertise in Diophantine equations and their formalization; the co-applicant provides expertise in proof automation and the development and use of proof assistants. Both aspects are crucial for the success of the project.

1.2 Ref 3:
His [Dahmens ref.] group was also involved in the creation of the aesop tactic

2.1 Ref 3:
The applicants rightfully point out that there is a societal impact, which lies both in the communication of results to a public of non-experts, 

2.2 Ref 3:
As noted by the applicants, the success of the project is a key to the adoption of proof assistant in other community of mathematician, with a potential impact on science in general.