Lychrel numbers in base 10

Exercise · rev10_120

Sanity check: digit reversal of 120 is 21.

Formal statement · Lean 4.lean

theorem rev10_120 : rev10 120 = 21 := by
  sorry

Proof. sorry

Nobody has tried yet.