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?