Proposal review

#Meta comments#

In many cases, the exposition of the task/goals is done directly, without context or preface, and then admits that, for example, the applicants already tackled these issues in some form. I think it would be better to preface things, saying we build on them and then mention the new challenges we are attacking. This would give a more positive narrative to the goal and tasks which is good. See for example:

Task 3
Ori. and innovation
I think both presentation are disjointly good and it is implicitly evident that they will probably benefit each other. I think however the proposal would benefit by making the links between the two projects clear.

General comments
Abstract

What does this mean?: At the same time, formalizing these aspects adds to the creation of a coherent library of mathematics in a rigorous logical language, whose merits go beyond obtaining a very high level of trust in the results.
In abstract, the link is not obvious. General automation is interesting for all mathematics. Why is diophantine equations a good field for these kind of automation? Why would it be a good guide? (We believe Diophantine equations will be a prime case study to guide the development of automation)
Background

In real life, proof assistent don't find new proofs. They close simple ones. Would maybe interesting to note that only some users with a very specific knowledge base can formalise post-graduate level mathematics. (For example, the new paper from Tao's A-team was formalised in lean. But there were many contributors, some one which, are professional formalisers!)

Does the jury know what is a computer algebra system?
Would be nice if the case study presented a clear near of some type of automation. I think we need to highlight this.
A.2. Design decision based on real mathematical uses
develop proof automation in the Lean proof assistant 
- Is there a stronger phrase we can use? (I find develop vague)
- Since Lean's automation is lacking in many aspects regarding the formalisation of post-graduate mathematics, we aim to create new solutions to succeed where today's automation comes short and apply this automation to verify computations and theorems related to Diophantine equations. 
Key obj. 3

For the more involved computations, we will aim at certifying external output data inside Lean, rather than running a formally verified algorithm inside the trusted kernel. In this way, we will benefit from the strong computer algebra systems already available, which provide fast implementations of a large collection of algorithms.

This is key, I would add a phrase before that says: But running formally verified algorithm is slow. We propose to implement reliable ways to create certificates that the algorithms are well behaved
Key obj. 4

What is more interesting? Building a library? Or achieving difficult results? My understanding is that papers in formalisations are focused on the latter.

This is laying the base for the theory of Diophantine equations. These are big theorem missing in lean.
- Could use words like celebrated, fundamental, etc.
Many interesting Diophantine equations could be considered. The choice will partly depend on library development, progress with other key objectives, and background knowledge or preference of the hired staff. 
- Is this ambitious enough?
Innovation

CoqHammer [34] for Coq has not been adopted by the community 
- Do we have any sources for this?

Granted, other proof assistants such as 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 target a much richer logic: Lean’s dependent type theory. This poses many new challenges. At the same time, dependent types are invaluable when developing a large, coherent library of formal mathematics. 
- I think this is important, but I think we could rephrase this a little bit. The issue is that isabelle is not expressive enough modern mathematics. Further more, the is nothing to admit as the automation added has the scientific value of solving new problems. This is the big issue.
- "The reason Isabelle provides good automation is that its logic is relatively simple in comparison to Lean's. In other words, it is an idealized setting for computer scientists. This, however, is unacceptable for mathematicians as they may not express their theorems and proofs in Isabelle. This is the challenge: Create a suitable adaptation of the hammer in this richer logic (Dependent type theory) whilst learning CoqHammer's failures."
A coherent formal library of fundamental and deep results for Diophantine equations 
Task 2

If we can be even more specific for the plan for auto, that would be nice
Task 3-4

- I would add a little sentence saying that many results about algebraic number theory are missing (despite Anne's best efforts)
- What is said on the math part and planification is very good but we are lacking a link with the other tasks! I think it would be important to specify where automatisation could be useful. For example we say
- "a unit group sieve (...) could take care of many tedious case distinctions
- This is a good idea (w/e it means) but we could also underline the fact that automatisation would be great once we have set up the correct case distinction allowing the problem to be solved mechanically (systematically)
- These projects have led to substantial results, on which we can now build.
- Like what (aesop maybe?)
Impact

We want to enable the number theory guys to focus on the real mathematical problems. Not the tedious tasks.
