I think you are misunderstanding the relationship between the theorem and the proof. You express doubt that the proof is a good one, but then you point to the libraries in Lean as a possible source of incorrectness. The libraries cannot be the source of incorrectness in the proof. They can only be the source of incorrectness in the statement of the theorem. That's why others are challenging you to declare that you don't trust the Lean kernel. A kernel bug is the only thing that can permit incorrectness in the proof.
The exact content of the proof doesn't matter for the purposes of deciding whether you should believe the theorem. At all. What matters are two things: 1) Is the theorem correctly stated? That is, does it say what it's supposed to say in the agreed upon (natural or programming) language? 2) Do you trust the Lean kernel (or human reviewer of the proof, if applicable)?
If you accept 1) and 2), then you must accept the truth of the theorem.
No library used in the construction of the proof, nor any library used in the expression or the proof, can make or break the result.
If one uses a library in the statement of the theorem, then that matters. That's letting someone else define some of the terms. And one must investigate whether those definitions are correct in order to decide whether the theorem is stated correctly. If you wish to challenge the work on these grounds, by all means proceed. But you can't say you don't think the proof is a good one for such reasons.
The exact content of the proof doesn't matter for the purposes of deciding whether you should believe the theorem. At all. What matters are two things: 1) Is the theorem correctly stated? That is, does it say what it's supposed to say in the agreed upon (natural or programming) language? 2) Do you trust the Lean kernel (or human reviewer of the proof, if applicable)?
If you accept 1) and 2), then you must accept the truth of the theorem.
No library used in the construction of the proof, nor any library used in the expression or the proof, can make or break the result.
If one uses a library in the statement of the theorem, then that matters. That's letting someone else define some of the terms. And one must investigate whether those definitions are correct in order to decide whether the theorem is stated correctly. If you wish to challenge the work on these grounds, by all means proceed. But you can't say you don't think the proof is a good one for such reasons.