Post #2141610
2025-04-07 14:05 UTC
@antoinechambertloir What does "not absolutely convincing" mean? I don't see a "sorry" in the pull request. Does "example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X])" not mean what it might appear? Or do you mean convincing of something else? Or do I just misunderstand how lean works?
Replies (1)
-
@antoinechambertloir@mathstodon.xyz 2025-04-07 15:50
@soaproot I mean that it takes some effort to treat this particular case, probably too much for what is worth. This indicates that one still needs to make automation better.