-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathreviews.txt
39 lines (30 loc) · 2.98 KB
/
reviews.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
p 7 l 46: "definitionally equal": I think this is the first time this phrase was used. You should explain what it means for the non-experts.
-> Explained in the last paragraph of section 3.2
p 7 l 54: "maps commute": I guess the word "commute" is used in the same sense as saying that diagrams commute, but is this a standard usage?
-> This is standard usage.
p 14 l 42-44: "However, it is quite challenging ...": this confused me. What is challenging about it? How is the product of submodules defined? Is it a matter of the difference between finite sets and finite sequences?
-> Clarified: we can't easily choose the finite sequence of coefficients
p 16 l 21: UFMs: it's a nice generalization. What are the other applications in mathlib? Anything other than nat and int?
-> Apart from instances for unique factorization *domains*, mathlib contains two instances for non-rings: `associates α` (the quotient of a monoid by the subgroup of invertible elements) and `ideal D` for a Dedekind domain `D` (and indeed if `D` is a principal ideal domain these two are isomorphic). We noew note these examples in section 4.4.
p 21 l 36: don't make me read the formal definition! Can you tell me what it says? The appearance of 'card' on line 40 was especially confusing, since I didn't notice it as an argument at first.
p 21 l 58: same comment: it would help to use words and an ordinary mathematical explanation.
-> We have expanded our explanation.
My main concern is how much the present submission extends the author's previous ITP article. As far
as I can see, most of the text is the same, and the new sections that were added (as described by
the authors) are concerned mainly with giving some more details on particular aspects of the same
formalization. The exception is Section 3.6, which describes work that was done after the previous
publication. I am not sure that this is enough to warrant a journal publication.
-> We have added a new Section 3 that gives a more comprehensive explanation of Lean and mathlib.
In particular, Section 3.1 provides a detailed explanation of typeclasses, including the choice between bundled and unbundled representations of mathematical structures.
An additional comment is that some familiarity with Lean is required in order to follow the
presentation; this should be mentioned explicitly - alternatively, the authors could consider
expanding their short presentation of the system (p.2, l.34-41). Likewise, it would be nice to have
a short introduction to the matlib library that is used throughout. However, these are minor
issues.
This is also addressed in Section 3.
Future directions: there are ongoing projects based on our formalization: adele/idele and FLT-regular.
-> Expanded section 8.1 by mentioning FLT regular, which builds on our work.
Other changes:
-> Explained details of the admissibility proof, including informal descriptions alongside formal Lean code.
-> typo and grammar fixes throughout
-> updated code samples to the latest mathlib version (let's say 2022-05-01)