Formal Verification of the Ward–Takahashi Identities in QED and QCD in Lean 4

We present a formal algebraic verification of the Ward–Takahashi identity in quantum electrodynamics (QED) and its analogue in quantum chromodynamics (QCD) using the Lean 4 proof assistant with the Mathlib library. The verification is carried out at tree level within a general algebraic framework: the Dirac algebra is modelled as an abstract F-algebra A, and gamma matrices as elements of A. The inverse fermion propagator is defined as S⁻¹(p) = p̸ − m. We prove that the contraction of the momentum transfer with the tree‑level vertex equals the difference of inverse propagators. For QCD, we extend the result to include colour generators, using the commutativity of the algebra map (which encodes the physical fact that colour and Dirac structures act on independent spaces). All proofs are checked by the Lean 4 kernel and depend only on Mathlib and the standard axioms (propext, Classical.choice, Quot.sound). The Lean source code is provided as supplementary material.