@antoinechambertloir@mathstodon.xyz
Post #2141608
2025-04-06 21:43 UTC
I made the fun last a bit longer by formalizing the proof in Lean, first of the generalized criterion, and then of the particular example.
It is not absolutely convincing, because Lean/Mathlib still lacks a bit of tools for handling explicit computations. And probably many parts can be streamlined.
Still, it was a fun exercise to do.
https://github.com/leanprover-community/mathlib4/pull/23710
Replies (2)
-
@antoinechambertloir@mathstodon.xyz 2025-04-06 22:25
A slightly edited version, with a formal statement can be found on my blog, Freedom Math Dance. https://freedommathdance.blogspot.com/2025/04/a-generalization-of-eisenstein-criterion.html
-
@soaproot@sfba.social 2025-04-07 14:05
@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?