Here is an example where finiteness is known, an algorithm exists, but such an algorithm is ineffective, in the sense that current computers (to my knowledge) won't terminate in any reasonable amount of time:
A Y-system associated to a Dynkin diagram Q of type ADE is a certain system of equations arising in physics. Given a fixed Q, it is known that
- there are finitely many positive integer solutions to the Y-system associated to Q, as such solutions are bounded below by 1 and bounded above by a constant say $c(Q)$.
- a brute-force algorithm defined by testing all values between 1 and $c(Q)$ works in principle.
- In general, the constant $c(Q)$ is in general ineffectively large, and far larger than the expected number of solutions (e.g. when $Q$ is of type $E_8$, one would have to test something like $2^{400000}$ values, whereas one "expects" far fewer solutions).