I recognized two of the lemmas (Lemmas 3.2 and 3.3) as doable with Walnut. It was very easy. Notice the usual trick of handling powers of the base; instead of writing powers as a function of k as in the paper, we merely assert that x or y is a power of 5 without specifying exactly which one it is. This is often good enough.
reg ispower5 msd_5 "0*10*":
# is argument a power of 5 ?
def ck "?msd_5 n=4*x":
# accepts c_k, where 5^{k-1} = x
def bk "?msd_5 5*x<=n & n<6*x":
# accepts members of B_k, where 5^{k-1} = x
def fk "?msd_5 10*x-1<=n & n<=15*x":
# accepts members of F_k, where 5^{k-1} = x
def ak "?msd_5 Ex $ispower5(x) & x<=y & (n=2 | n=3 | $ck(n,x) | $bk(n,x) | $fk(n,x))":
# accepts members of A_k, where 5^{k-1} = y
def a "?msd_5 Ey $ispower5(y) & $ak(n,y)":
# accepts members of A
eval lemma32 "?msd_5 Ay,n (4<=n & n<=6*5*y & $ispower5(y)) => En1, n2 $ak(n1,y) & $ak(n2,y) & n=n1+n2":
def jk "?msd_5 9*x<=n & n<10*x":
# accepts members of J_k, where x = 5^{k-1}
eval lemma33 "?msd_5 An,y,c,d ($ispower5(y) & $jk(n,y) & $a(c) & $a(d) & n=c+d)
=> (($ck(c,y) & $bk(d,y)) | ($ck(d,y)|$bk(c,y)))":