Important open problems that have already been reduced to a finite but infeasible amount of computation Most open problems, when formalized, naturally involve quantification over infinite sets, thereby obviating the possibility, even in principle, of "just putting it on a computer."
Some questions (e.g. the existence of a projective plane of order 12) naturally resolve after a finite computation but not feasibly.
I'd like examples of reasonably important open problems that have now been reduced, via nontrivial arguments, to finite but infeasible computations. 
I'm sure that additive number theory gives examples (certain questions along the lines of Goldbach conjecture and Waring's problem, but I don't have the details handy).  I'd love especially to see examples that don't seem to originate in discrete mathematics.
 A: In Conway's Game of Life, a lot of active problems are related to reducing the size of currently known types of starting states:

*

*It's well-known that there are diagonal (e.g. glider) and orthogonal (e.g. Conway's "lightweight spaceship") spaceships, and these are quite small. It was unknown whether there were any spaceships that travel at any slopes other than these eight basic slopes, until the Gemini (which moves at a slope of five-to-one) was constructed as late as in 2010! Gemini's starting position is massive and doesn't fit inside a box of $10^6\times 10^6$ cells, so improving the size of such a spaceship was a problem among Life enthusiasts. This problem was greatly improved by computer search, resulting in Sir Robin, which moves in the direction of a knight (two-to-one slope.) Finding another so-called "knightship" that fits within Sir Robin's bounding box would require at most a naive brute-force search of $2^{31\times 79}$ positions.

*A Garden of Eden is a state that is not the image of some previous state. The smallest known Garden of Eden is this one,
and details can be found here. Finding a smaller GoE is a straightforward computer search with an explicit upper bound: $2^{10\times 10}$ states needs to be examined, at most. The smallest known example was found by searching for GoE with an additional symmetry, and is thus the smallest symmetric (in some sense) GoE.

A: Computing homotopy groups of spheres has been reduced in several different ways down to a finite but infeasible computation. This was discussed in another thread. John Klein's answer describes an algorithm Dan Kan came up with. The accepted answer points to other work which contains a more efficient method, but which I haven't read. I suppose you could argue that this is not an important enough problem (actually, this has also been done on MathOverflow), but most topologists would disagree. Certainly this is not a problem which originates in discrete math.
A: Baker's work on linear forms in logarithms reduced great big families of diophantine equations to finite searches. In many cases, sharpening of Baker's results plus large amounts of cleverness have brought the computations into the feasible range, but many other cases are still infeasible. 
A: Numerical evidence suggested $\pi(x)$ is always less than $\mathrm{li}(x)$.
Littlewood proved that $\pi(x) - \mathrm{li}(x)$ changes sign infinitely often, but the smallest $x$ s.t. 
$\pi(x) > \mathrm{li}(x)$ is currently not known.
The smallest such $x$ is 
Skewes' number 
There is a crossing near $e^{727.95133}$. It is not known whether it is the smallest.
The problem possibly might be solved by some clever method other than naiively computing $\pi(x)$,
but I don't see why this argument doesn't apply to the other answers.
A: One of the most important open questions in graph theory is Hadwiger's conjecture, which asserts that every graph with no $K_{t}$-minor is $(t-1)$-colourable.  The cases $t=1,2$ are trivially trivial, and the case $t=3$ is trivial.  The case $t=4$ was actually proved by Hadwiger himself.  The case $t=5$ was proved by Wagner to be equivalent to the Four colour theorem (and hence is true).  The case $t=6$ was proved to hold by Robertson and Seymour and also uses the Four colour theorem.  The case $t=7$ is open.  
This naturally leads us to the question of given a fixed $t$, does Hadwiger's conjecture hold for $t$?  Reed and Kawarabayashi proved that this question can be solved with a finite amount of computation.  Namely, they prove: 


*

*There is a computable function $f(t)$ such that every minimal counterexample to Hadwiger's conjecture for $t$, has at most $f(t)$ vertices.  

*For any fixed $t$, there is an $O(n^2)$-algorithm to decide if a graph with $n$ vertices is a counterexample to Hadwiger's conjecture for $t$.
Therefore, for any fixed $t$, Hadwiger's conjecture can be decided in finite time (but the amount of time is currently infeasible).  
A: In principle, any mathematical question $\psi$ that is not independent of ZFC (or some standard stronger theory, such as ZFC+large cardinals) is reducible to the finite computational procedure: search for a proof of $\psi$ or a proof of $\neg\psi$. If the statement is not independent, then we will find one or the other; but such computation procedures are generally infeasible, with no known bound on their length. Meanwhile, if $\psi$ is provably independent of ZFC, then we may search for a proof of that. But alas, if our axioms are consistent, then some statements may be independent, but not provably so, and we can prove that if our axioms are consistent, then there will be such examples. 
Meanwhile, there are many interesting and useful theories that have been proved to be decidable, but which have infeasible decision procedures. For example, any question of Cartesian geometry in any finite dimension is decidable in principle by computational means, since the theory of real-closed fields is decidable, meaning that in principle, we can decide the truth of any assertion expressible in the structure $\langle\mathbb{R},{+},{\cdot},{\lt},0,1\rangle$, which includes many interesting statements, many of which are natural open problems of the kind you seek, such as almost all the famous packing problems. Unfortunately, the best-known algorithms for this decision procedure are at least double-exponential time, and hence infeasible. Similarly, the theory of abelian groups is decidable; Presburger arithmetic is decidable; the theory of infinite chess is decidable and many other interesting theories, capable of expressing many natural problems. 
So there would seem to be an abundance of examples of the type you seek.
A: Computing Ramsey numbers or even tighter bounds on them is perhaps a prototypical example that fits the bill.
A: Jacobsthal's function $g(n)$ for a positive integer $n$ gives the smallest number $g$ such that any interval of consecutive integers of length $g$ contains an integer coprime to $n$.  I have been working on bounding this function for a while now, hoping to beat lower bounds near $k \log k$ (many researchers, most recently Konyagin-Ford-Green-Maynard-Tao) and upper bounds $(k\log k)^2$ (Iwaniec), where $k$ is the number of distinct prime factors of $n$.
Some have wondered about Jacobsthal's $C(k)$, which is the maximum over all $n$ with $k$ distinct prime factors of $g(n)-1$.  (Read Jacobsthal's 1961 paper for why this definition.)
It is not immediately clear that one should check only finitely many cases to determine $C(k)$, however a nice argument in Hajdu and Saradha's paper "Disproof of a Conjecture of Jacobsthal" shows that indeed only a finite number of $n$ need to be checked.  Further, the maximum does not always occur at $n =P_k= \prod_{1 \leq i \leq k} p_i$, the product of the first $k$ primes.  Although exact computations have been carried out for $k \lt 50$ for $g(P_k)$, $C(k)$ seems to be known only up to $k=24$.
Gerhard "Ask Me About Jacobsthal's Function" Paseman, 2015.05.15
A: Thurston asked for the maximal number of non-hyperbolic Dehn fillings on a one-cusped hyperbolic 3-manifold, and conjectured that the maximum is 10 which is only achieved by the figure eight knot complement. It's now been shown that the maximum is 10 by Lackenby-Meyerhoff, but I've also shown that there is an algorithm which will determine the finitely many manifolds with $>8$ exceptional Dehn fillings.
A: You mention additive number theory in the question, so perhaps this isn't the type of example that you want. However my understanding is that the Three Primes Conjecture (every odd number $\geq 7$ is the sum of three primes) is now at the cusp of a feasible computer solution.
Vinogradov proved that the conjecture was true for all sufficiently large odd numbers (i.e. there exists $C>0$ such that every odd number greater than $C$ is the sum of three primes).
Various people have given explicit values for $C$ but, up until recently, the best (i.e. lowest) explicit value was $e^{3100}$. This is still, obviously, way out of computational range. 
However Tao and, then, more recently Helfgott have improved these bounds by studying so-called `minor arcs', so that now one could just about imagine dealing with remaining cases via computer.  The results of Helfgott are expressed in terms of a parameter $q$ pertaining to minor arcs. His work implies that the conjecture is true for $q>4\cdot 10^6$.
If you're interested you should read Helfgott's preprint which begins with a brief summary of the history of this problem.
EDIT: and since then it has been resolved: http://arxiv.org/abs/1501.05438 .  Congratulations to Prof. Helfgott.
A: Voronoi gave an algorithm to enumerate all perfect quadratic forms in $n$ variables and consequently to identify the densest lattice packing of spheres in $\mathbb{R}^n$.
A: I am not sure if this fits all the stated criterions but since it is a neat problem here it goes..
Is there a 57-regular graph  $X$ of order 3250 , girth 5 and diameter 2?
$X$ is known as a Moore graph
A lot is known about $X$ (automorphism group has order less than 350), independence number is at most 400, the chromatic polynomial is $(x-57)(x+8)^{1520}(x-7)^{1729}$, but the search space of all potential graphs is still too large to be computed with an algorithm.
A: As a result of Terry Tao's recent blog post the lonely runner conjecture for any particular value of $n$ has been reduced to a finite computation. Currently the LRC is verified only for $n \leq 7$.
A: This is an elaboration of a comment on Suvrit's answer. 
Ramsey numbers can be defined for (infinite) ordinals, just as in the finite case: $r(\alpha,\beta)$ is the least $\gamma$ such that for any $2$-coloring of the edges of the complete graph on $\gamma$ vertices there is a set of vertices of type $\alpha$ whose induced graph is red, or a set of vertices of type $\beta$ whose induced graph is blue. 
Ramsey's theorem gives that $r(\omega,\omega)=\omega$, but already $r(\omega+1,\omega)=\omega_1$. On the other hand, if $\alpha\lt\omega_1$ and $n$ is finite, then $r(\alpha,n)\lt\omega_1$, and for reasonably small infinite values of $\alpha$, one can attempt to compute $r(\alpha,n)$ explicitly. It turns out that this computation reduces to (Ramsey-theoretic) finite problems, which, just as with the classic computation of finite Ramsey numbers, quickly become unfeasible. 
For example:


*

*$r(\omega+3,3)=\omega\cdot2 + 8$. In general, if $0\lt n,m\lt\omega$, then
$$ r(\omega+n,m)=\omega\cdot(m-1)+(g(n,m)-(m-1)), $$
where $g(n,m)$ is the least $k$ such that any $2$-coloring of the edges of the complete graph on set of vertices $\{1,\dots,k\}$ such that the induced graph on $C=\{1,\dots,m-1\}$ is blue, either admits a blue $K_m$, or a red $K_{n+1}$ with one of its vertices in $C$.


This was first established by Haddad and Sabbagh in 1969. One has $r(n+1,m)\le g(n,m)\lt\infty$, but typically the first inequality is strict. For example, $r(4,3)=9$ but $g(3,3)=10$. In general, computing $g(n,m)$ is similar to, but harder than computing $r(n+1,m)$. 


*

*$r(\omega\cdot3,3)=\omega\cdot9$. In general, if $0\lt n,m\lt\omega$, then 
$$ r(\omega\cdot n,m)=\omega\cdot l(n,m), $$
where $l(n,m)$ is the least $k$ such that any $2$-coloring of the edges of the complete digraph on $k$ vertices either contains a red complete digraph on $n$ vertices, or a blue transitive tournament on $m$ vertices. 


Here, in complete digraphs we have two arrows (going in opposite directions) between any two distinct vertices. This was shown by Erdős and Rado in 1955. As with $g$, the computation of the values of $l(n,m)$ quickly becomes unfeasible.


*

*$r(\omega^2\cdot2,3)=\omega^2\cdot10$. In general, if $0\lt n,m\lt\omega$, then $r(\omega^2\cdot m,n)=\omega^2\cdot h(m,n)$ for a Ramsey-theoretic function $h$ related to $3$-colorings of the edges of digraphs, though its exact description is somewhat technical to include here. This was shown fairly recently by Thilo Weinert, see here. 

A: At the turn of the 21st century, Catalan's conjecture that $8$ and $9$ are the only non-trivial consecutive powers was reduced to a finite but intractable problem.   
For example, it was known that to prove that
$$3^2-2^3=1$$
are the only non-trivial integral solutions to 
$$x^p-y^q=\pm 1$$
required checking a finite number of $p$'s and $q$'s with $\max(p,q)=8\times10^{16}$.
However, in 2002 Mihăilescu proved the conjecture in its entirety.
See, e.g., Metsänkylä's AMS article, especially § 4 titled "Can the Problem be Solved by a Computer?"
Although it's not 'open', I think this is in the spirit of the question.
A: It is thought that it is more difficult to calculate the permanent of an $n\times n$ matrix than to calculate the determinant of the matrix. 
However, even for $4\times 4$ matrices this problem seems far out of reach - calculating the determinant of a $4\times 4$ matrix requires least 37 arithmetic operations, yet it would naively require evaluating about $10^{123}$ different programs to prove that the permanent of a $4\times 4$ matrix cannot be calculated in 37 or fewer operations.  See Aaronson's slides from 2007.
(I know this doesn't perfectly fit the desiribles of the OP, but at least it's a reasonably important open problem outside of additive number theory that is finite but presently infeasible.)
