Zulip Chat Archive

I've come to Lean via the Aristotle AI tool to formalize proofs. I have a project to formalize a proof of an empirical rule or conjecture appearing in a Math. Stack Exchange posthttps://math.stackexchange.com/questions/5075981/how-to-determine-which-of-two-conjugate-roots-is-the-frobenius-of-alpha, for which ChatGPT has an informal proof.
I've got several lemmas that compile successully with the Linux command: lake build. However, one troublesome lemma in elementary commutative algebra won't compile. I'm attaching a statement and proof of this lemma as a PDF that I undertand myself.
LU_equiv_lemma_writeup_2026-01-17.pdf
My math background is in functional analysis, and I have a 2-year certificate in computer science. I'm from Quebec in Canada.

Snir Broshi (Jan 18 2026 at 01:13):

Hello :wave:
What's the question? What have you tried other than a blackbox lake build? Did you read the AI generated code?
Can you include more details in general? I think #PrimeNumberTheorem+ > Duality principle @ 💬 is a nice example from today on adding detail to a question.

David Bernier (Jan 18 2026 at 04:51):

Hello, I'd like to know where I can find simple proofs in Lean about polynomial rings (Z/nZ)[x]? I tried editing the module that won't compile based on the compilation error messages, and got rid of some errors, but not all. I tried connecting Linux to Windows Visual Code, but I don't like Visual Code. For now, I'll stick to lake build in Linux.

P.S. I'd have use for this result: "In a commutative ring, let u be a unit and suppose a*b = u. Then a is also a unit." Perhaps it's already in Mathlib?