For a decision problem, if a mathematician finds a simple polynomial time procedure that solves it, does it mean that the problem is polynomial time solvable?
For example, consider a decision problem: whether there exists a vector $(x_1, x_2, ..., x_K)$ such that $f(x_1, x_2, ..., x_K, d, M, N)=0$, where $d, M, N$ are parameters, and $f$ is a given function.
Suppose that a mathematician proves that the answer is yes iff $M+N \geq d(K+1)$. Then, can we say that the decision problem is polynomial time solvable?
If so, then I would be puzzled by another example I could think of, which involves Fermat's Last Theorem. We can pose the theorem as a question decision problem: whether we can find positive integers $a,b,c$ such that $a^n + b^n = c^n$ for a given positive integer $n$. The size of the problem is $n$. The problem was solved by mathematician Wiles in 1997: the answer is yes if $n=1$ or $2$, and is no otherwise. This answer can be easily written as a line of code in a regular computer (or a very simple program in a Turing Machine), and the time complexity is certainly polynomial. So can we say that a Turing Machine can solve Fermat's Last Theorem in polynomial time (actually constant time), even though it took mathematicians centuries to solve it?
I think there's some confusion about terminology, as copper.hat and dfeuer point out.
Let's define a problem to be sets $I,O$ of inputs and outputs, together with a function $P:I\to O$ which defines the unique correct output for a given input. We assume elements of $I$ can be measured (by the number of bits $n$ they are encoded in, say) in some way. Then we can say the problem $(I,O,P)$ is polynomial time solvable is there exists a Turing machine which can process $i\in I$ in a number of operations at most polynomial in $n$ and leave $P(i)$ on the tape.
In other words, a problem is polynomial time solvable if some genius could invent a Turing machine which responds correctly to every possible input quickly enough.
The key thing here is what are the range of inputs?
Yes, if a civilization of mathematicians spends a thousand years developing the machinery to prove that $P(1) = P(2) = \text{yes}$ and $P(i) = \text{no}$ otherwise, then the decision problem "Is there an interesting solution to $a^i + b^i = c^i$?" taking $i \in\{1,2,\ldots\}$ to $\{\text{yes},\text{no}\}$ is polynomial time solvable. Very trivially.
By contrast, the decision problem "Is there an interesting solution to the formula $i$?" where $i\in I$ is an arbitrary problem which is specified as input, then you're probably not going to get a simple solution! (See the Boolean case mentioned by Andreas Blass for example).