Formalizing a ring theorem with Lean 4 and Claude

A user tested Claude's ability to generate Lean 4 code to formalize a ring theorem, achieving a proof after 11 iterations but with five unproven 'sorry' sections. The experiment highlights challenges in AI-assisted formal verification, including hallucinations and dependency issues with Mathlib.

I’ve been testing Claude’s ability to generate Lean 4 code to prove theorems. I’ve written about a couple https://www.johndcook.com/blog/2026/06/10/claude-and-lean/ experiments https://www.johndcook.com/blog/2026/06/15/quaternions-claude-lean/ that verified calculations. I did not write about my failed attempt to get Claude to formalize a proof of the pqr theorem https://www.johndcook.com/pqr theorem.pdf for seminorms. This time I asked Claude to formally prove the theorem from the previous post on partial fraction decomposition https://www.johndcook.com/blog/2026/06/16/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. python /- PartialFractions.lean v11 — final -/ import Mathlib open UniqueFactorizationMonoid variable {R : Type } CommRing R IsDomain R IsPrincipalIdealRing R structure PFDSummand R : Type CommRing R where prime : R exponent : ℕ numer : R noncomputable def PFDSummand.val CommRing R IsDomain R s : PFDSummand R : FractionRing R := algebraMap R FractionRing R s.numer / algebraMap R FractionRing R s.prime ^ s.exponent structure IsPFD CommRing R IsDomain R IsPrincipalIdealRing R terms : List PFDSummand R c : FractionRing R : Prop where irred : ∀ s ∈ terms, Irreducible s.prime nonAssoc : ∀ s ∈ terms, ∀ t ∈ terms, s ≠ t → ¬Associated s.prime t.prime coprime : ∀ s ∈ terms, IsCoprime s.numer s.prime sum eq : terms.map PFDSummand.val .sum = c private lemma algMap ne zero {a : R} h : a ≠ 0 : algebraMap R FractionRing R a ≠ 0 := map ne zero iff IsFractionRing.injective R FractionRing R | .mpr h private lemma exists num denom c : FractionRing R : ∃ a b : R, b ≠ 0 ∧ algebraMap R FractionRing R a / algebraMap R FractionRing R b = c := by obtain ⟨a, b, hb, hab⟩ := IsFractionRing.div surjective A := R c exact ⟨a, b, nonZeroDivisors.ne zero hb, hab⟩ -- ====================================================================== -- §6 Bézout splitting -- ====================================================================== private lemma bezout split x y : R hcop : IsCoprime x y hx : x ≠ 0 hy : y ≠ 0 e : R : ∃ s t : R, s x + t y = 1 ∧ algebraMap R FractionRing R e / algebraMap R FractionRing R x algebraMap R FractionRing R y = algebraMap R FractionRing R e t / algebraMap R FractionRing R x + algebraMap R FractionRing R e s / algebraMap R FractionRing R y := by obtain ⟨s, t, hst⟩ := hcop refine ⟨s, t, hst, ? ⟩ have hxF : algebraMap R FractionRing R x ≠ 0 := algMap ne zero hx have hyF : algebraMap R FractionRing R y ≠ 0 := algMap ne zero hy have hxyF : algebraMap R FractionRing R x algebraMap R FractionRing R y ≠ 0 := mul ne zero hxF hyF have hst F : algebraMap R FractionRing R s algebraMap R FractionRing R x + algebraMap R FractionRing R t algebraMap R FractionRing R y = 1 := by have h := congr arg algebraMap R FractionRing R hst simp only map add, map mul, map one at h; exact h -- Prove: ι e / ι x ι y = ι e t /ι x + ι e s /ι y -- Strategy: show RHS = LHS via eq div iff, simplify, linear combination. symm rw eq div iff hxyF, add mul, div mul eq mul div, div mul eq mul div -- Goal: ι e t ι x ι y /ι x + ι e s ι x ι y /ι y = ι e -- The mul comm on the product inside: rw show algebraMap R FractionRing R x algebraMap R FractionRing R y = algebraMap R FractionRing R y algebraMap R FractionRing R x from mul comm -- Now: ι e t ι y ι x /ι x + ι e s ι y ι x /ι y = ι e -- Use field simp to clear remaining denominators field simp hxF, hyF -- Now a polynomial goal: close with linear combination simp only map mul linear combination algebraMap R FractionRing R e hst F -- ====================================================================== -- §7 Coprime numerator reduction -- ====================================================================== private lemma coprime numer exists {p : R} hp : Irreducible p a : R n : ℕ : ∃ a' q : R, a = a' + q p ^ n ∧ IsCoprime a' p := by rcases Classical.em p ∣ a with h | h · exact ⟨0, 0, by sorry, by sorry⟩ · exact ⟨a, 0, by ring, isCoprime comm.mpr irreducible iff prime.mp hp .coprime iff not dvd.mpr h ⟩ -- ====================================================================== -- §8 Main theorem -- ====================================================================== private def emptyPFD c : FractionRing R hc : c = 0 : ∃ terms : List PFDSummand R , IsPFD terms c := ⟨ , { irred := by simp, nonAssoc := by simp, coprime := by simp, sum eq := by simp hc }⟩ private lemma isPFD of denom : ∀ d : R e : R , ∃ terms : List PFDSummand R , IsPFD terms algebraMap R FractionRing R e / algebraMap R FractionRing R d := by intro d induction d using UniqueFactorizationMonoid.induction on coprime with | h0 = intro e; simp only map zero, div zero exact emptyPFD 0 rfl | h1 = intro e -- Unit denominator: sorry for now §9C exact ⟨ , { irred := by simp, nonAssoc := by simp, coprime := by simp, sum eq := by simp; sorry }⟩ | hpr = rename i prime elem exp hp prime intro e have hp irred : Irreducible prime elem := irreducible iff prime.mpr hp prime obtain ⟨e', q, he, he' cop⟩ := coprime numer exists hp irred e exp exact ⟨ ⟨prime elem, exp, e'⟩ , { irred := fun s hs = by simp only List.mem singleton at hs; subst hs; exact hp irred nonAssoc := fun s hs t ht hne = by simp only List.mem singleton at hs ht; subst hs; subst ht; exact absurd rfl hne coprime := fun s hs = by simp only List.mem singleton at hs; subst hs; exact he' cop sum eq := by simp only List.map singleton, List.sum singleton, PFDSummand.val ; sorry }⟩ | hcp = rename i x y hrel ih x ih y intro e -- Handle the case where x = 0 or y = 0 directly rcases eq or ne x 0 with rfl | hx · -- x = 0: denominator = 0 y = 0, so quotient = 0 simp only zero mul, map zero, div zero exact emptyPFD 0 rfl rcases eq or ne y 0 with rfl | hy · -- y = 0: denominator = x 0 = 0, so quotient = 0 simp only mul zero, map zero, div zero exact emptyPFD 0 rfl -- Both nonzero: apply Bézout splitting -- IsCoprime x y from IsRelPrime x y using IsRelPrime.isCoprime have hcop : IsCoprime x y := hrel.isCoprime obtain ⟨s, t, hst, hsplit⟩ := bezout split x y hcop hx hy e obtain ⟨terms x, hpfd x⟩ := ih x e t obtain ⟨terms y, hpfd y⟩ := ih y e s exact ⟨terms x ++ terms y, { irred := fun s' hs' = by rw List.mem append at hs' exact hs'.elim hpfd x.irred s' hpfd y.irred s' nonAssoc := fun s' hs' t' ht' hne = by rw List.mem append at hs' ht' rcases hs' with hs' | hs' <; rcases ht' with ht' | ht' · exact hpfd x.nonAssoc s' hs' t' ht' hne · intro; sorry · intro; sorry · exact hpfd y.nonAssoc s' hs' t' ht' hne coprime := fun s' hs' = by rw List.mem append at hs' exact hs'.elim hpfd x.coprime s' hpfd y.coprime s' sum eq := by rw List.map append, List.sum append, hpfd x.sum eq, hpfd y.sum eq -- Goal: ι e t /ι x + ι e s /ι y = ι e / ι x y -- hsplit: ι e/ ι x ι y = ι e t /ι x + ι e s /ι y -- So: ι e t /ι x + ι e s /ι y = ι e/ ι x ι y = ι e/ι x y rw ← hsplit, map mul }⟩ theorem pid partial fraction decomposition c : FractionRing R : ∃ terms : List PFDSummand R , IsPFD terms c := by obtain ⟨a, b, hb, hc⟩ := exists num denom c rw ← hc ; exact isPFD of denom b a section IntExample example c : FractionRing ℤ : ∃ terms : List PFDSummand ℤ , IsPFD terms c := pid partial fraction decomposition c end IntExample