Let $a_n$ and $b_n$ be two different expressions in natural $n$ with values in the set of all nonnegative integers such that we have the identity $a_n=b_n$ for all $n$. As a simplest example, we may consider $a_n:=\sum_{k=0}^n\binom nk$ and $b_n:=2^n$.
Is there an automated, algorithmic construction of bijective proofs of broad enough classes of such identities?
Given $a_n$ and $b_n$, such an algorithm would parse the expressions $a_n$ and $b_n$ and then (i) construct finite sets $A_n$ and $B_n$, (ii) construct a bijection from $A_n$ onto $B_n$, and (iii) show that the cardinalities of $A_n$ and $B_n$ are $a_n$ and $b_n$, respectively.
Remark: To avoid undesirable, trivial constructions such as the one mentioned in a comment by Sam Hopkins, it should be required that the expressions for the sets $A_n$ and $B_n$ not contain the expressions $a_n$ and $b_n$ as terms.
Weaker versions of the above question are obtained by asking the steps (i)–(iii) to be done only for all small enough values of $n$, possibly followed by a conjecture for all $n$.
The above question is, of course, somewhat vague, because it is hard to attach in advance a definite meaning to the phrase "broad enough classes".
In 2017, Timothy Chow asked a related question Automated search for bijective proofs, which was well thought-out and well presented. The main difference is that there sets $A_n$ and $B_n$ were given.
Even with $A_n$ and $B_n$ given, the problem appears very difficult. However, there may have been progress on such problems since 2017.
