Some flaws in Munkres.lean

[Hziwara]

I have found the following flaws in the formal translation of exercises from Munkres' textbook. While some are only a matter of faithfulness to the original, some make propositions implausible.

• 13_3b: This formalization is not faithful since the original does not indicate which property of topology fails.
• 13_4b1, 13_4b2: The directions of the last inclusions seem to be reversed.
• 13_5a, 13_5b: The formalized statements are weaker than the original because the formers consider generated topology from intersection, while the latters do intersection itself.
• 13_8b: The formalized statement is weaker because the original says also that the set is a basis of some topology.
• 16_1: I cannot understand this translation. The formalized statement seems to be different from the original and even wrong.
• 16_6: The right arrow in hS should be replaced by \iff.
• 18_13: The formalized statement lacks the assumption that $g$ and $g'$ are extensions of $f$.
• 19_6a: Although the product is not assumed to be finite in the original statement, the formalized one assumes it.
• 22_2a: The formalized statement is stronger than the original because it says 'if and only if' instead of 'if'. I believe that the inverse does not hold generally.
• 22_5: The codomain of $q$ should be $p(A)$, not $Y$, although it does not affect truth in this case.
• 23_3: Although $A$ is not assumed to be countable in the original statement, the formalized one assume it.
• 23_4: The original statement does not say about all subsets of $X$ but only $X$ itself.
• 23_9: The original statement considers only the cases of $X=A_2$ and $Y=B_2$.
• 24_2 : $S^1$ is a circle on the plane, not a subset of \R.
• 24_3a: I cannot understand why the topology of $I$ is an argument in the formal statement. The only natural one should be considered.
• 26_12: The formalized statement lacks the assumption that $p$ is a closed map.
• limit_point_compact: The notion of limit point seems to correspond to AccPt in Mathlib, not to ClusterPt.
  • https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Defs/Filter.html#ClusterPt
• 28_5: The direction of inclusion relation for $C$ seems to be reversed.
• 29_4: While the original statement considers the uniform topology, the formalized statement does not specify topology.
• 30_13: The formalized statement lacks the assumption that all elements of $U$ are open.
• 34_9: The formalized statement lacks the assumption that $X$ is Hausdorff.
• 43_2: The domain of f and g should be A and closure A, respectively. Moreover, the formalized statement is slightly weaker than the original one, since the former says that uniformly continuous extension is unique but the latter says that the continuous extension is already unique.

In addition, natural language proofs sometimes refer to theorems or exercises excluded from the benchmark by labels in the textbook, which makes it difficult to autoformalize proofs without retrieval from the textbook.

[BartoszPiotrowski]

Hi @Hziwara, thank you very much for pointing at these mistakes! We are determined to fix all of that, we are going to look into it soon. If you see any other flaws, please, let us know.

[zhangir-azerbayev]

Hi @Hziwara, thanks for catching these. Maintenance of this repo is paused while we figure out whether to merge the Lean 4 translation from https://github.com/rahul3613/ProofNet-lean4 or archive this repo in favor of it. If the issues you've raised persist in the Lean 4 version, we'll make sure to correct them.