Formalizing a ring theorem with Lean 4 and Claude

(832) 422-8646

Contact

I’ve been testing Claude’s ability to generate Lean 4 code to prove theorems. I’ve written about a couple experiments that verified calculations. I did not write about my failed attempt to get Claude to formalize a proof of the pqr theorem for seminorms.

This time I asked Claude to formally prove the theorem from the previous post on partial fraction decomposition in an abstract setting. Unlike the previous experiments, I did not give it a proof or calculation to verify; I asked it to generate a proof.

This was the prompt:

Write a proof in Lean 4 for the following generalization of partial fraction decomposition.

If a ring R is a principle ideal domain (PID), then every element c of the field of fractions over R can be written in the form \[c = \sum_i \frac{a_i}{p_i^{r_i}}\]

where the p_i are nonassociate irreducible elements of R, the r_i are non-negative integers, and the elements a_i and p_i are relatively prime.

This was Claude’s immediate response:

I’ll work through this carefully, as it’s a substantial formalization task. Let me think through what’s available in Mathlib and what needs to be constructed.

This is a genuinely hard Lean 4 formalization problem. Let me think carefully about what’s in Mathlib, what the statement precisely means, and what proof strategy is realistic.

It also stated its overall proof strategy:

Proof strategy : Write c = a/b in lowest terms. Factor b = ∏ pᵢ^rᵢ. Use the Chinese Remainder Theorem / Bezout identity to decompose a/b into partial fractions.

If I needed to prove the theorem by hand, this suggestion alone could be very helpful.

The first attempt generated code that would not build. As before, a lot of the problems seem to stem from things moving around in Mathlib due to refactorings. There are also occasional hallucinations.

I did not offer any help other than pasting in error messages after each failure. When working on a real problem, I’d be more interactive. But as a test, I just passively pasted error messages and tried again. It took 11 iterations, but I finally got a proof. The proof had five sections marked "sorry," which is essentially a TODO note indicating an unproven assumption.

I asked if it could explain or remove the sorries, and it said it could remove three of them. But the generated code did not build and I hit a session limit before I could debug the code. Here is the code with five sorry sections.

/-<br>PartialFractions.lean (v11 — final)<br>-/

import Mathlib

open UniqueFactorizationMonoid

variable {R : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]

structure PFDSummand (R : Type*) [CommRing R] where<br>prime : R<br>exponent : ℕ<br>numer : R

noncomputable def PFDSummand.val [CommRing R] [IsDomain R] (s : PFDSummand R) :<br>FractionRing R :=<br>algebraMap R (FractionRing R) s.numer /<br>algebraMap R (FractionRing R) (s.prime ^ s.exponent)

structure IsPFD [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]<br>(terms : List (PFDSummand R)) (c : FractionRing R) : Prop where<br>irred : ∀ s ∈ terms, Irreducible s.prime<br>nonAssoc : ∀ s ∈ terms, ∀ t ∈ terms, s ≠ t → ¬Associated s.prime t.prime<br>coprime : ∀ s ∈ terms, IsCoprime s.numer s.prime<br>sum_eq : (terms.map PFDSummand.val).sum = c

private lemma algMap_ne_zero {a : R} (h : a ≠ 0) :<br>(algebraMap R (FractionRing R)) a ≠ 0 :=<br>map_ne_zero_iff _ (IsFractionRing.injective R (FractionRing R)) |>.mpr h

private lemma exists_num_denom (c : FractionRing R) :<br>∃ a b : R, b ≠ 0 ∧<br>(algebraMap R (FractionRing R)) a / (algebraMap R (FractionRing R)) b = c := by<br>obtain ⟨a, b, hb, hab⟩ := IsFractionRing.div_surjective (A := R) c<br>exact ⟨a, b, nonZeroDivisors.ne_zero hb, hab⟩

-- §6 Bézout splitting

private lemma bezout_split (x y : R) (hcop : IsCoprime x y)<br>(hx : x ≠ 0) (hy : y ≠ 0) (e : R) :<br>∃ s t : R, s * x + t * y = 1 ∧<br>(algebraMap R (FractionRing R) e) /<br>((algebraMap R (FractionRing R) x) * (algebraMap R (FractionRing R) y)) =<br>(algebraMap R (FractionRing R) (e * t)) / (algebraMap R (FractionRing R) x) +<br>(algebraMap R (FractionRing R) (e * s)) / (algebraMap R (FractionRing R) y) := by<br>obtain ⟨s, t, hst⟩ := hcop<br>refine ⟨s, t, hst, ?_⟩<br>have hxF : (algebraMap R (FractionRing R)) x ≠ 0 := algMap_ne_zero hx<br>have hyF : (algebraMap R (FractionRing R)) y ≠ 0 := algMap_ne_zero hy<br>have hxyF : (algebraMap R (FractionRing R)) x *<br>(algebraMap R (FractionRing R)) y ≠ 0 := mul_ne_zero hxF hyF<br>have hst_F : (algebraMap R (FractionRing R)) s * (algebraMap R (FractionRing R)) x +<br>(algebraMap R (FractionRing R)) t * (algebraMap R (FractionRing R)) y = 1 := by<br>have h := congr_arg (algebraMap R (FractionRing R)) hst<br>simp only [map_add, map_mul, map_one] at h; exact h<br>-- Prove: ι e / (ι x * ι y) = ι(e*t)/ι x + ι(e*s)/ι y<br>-- Strategy: show RHS = LHS via eq_div_iff, simplify, linear_combination.<br>symm<br>rw [eq_div_iff hxyF, add_mul, div_mul_eq_mul_div, div_mul_eq_mul_div]<br>-- Goal: ι(e*t)*(ι x*ι y)/ι x + ι(e*s)*(ι x*ι y)/ι y = ι e<br>-- The mul_comm on the product...