There are certain mathematical statements and problems that cannot be proven or solved using formal proofs within a given axiomatic system. This fundamental limitation of formal systems was demonstrated by Alan Turing and others in the 1930s.
Turing's work on the Entscheidungsproblem ("decision problem") showed that there is no general method or algorithm that can determine whether an arbitrary mathematical statement is provable or not.
Specifically, he proved that the halting problem - determining whether a given Turing machine will halt on a given input - is undecidable.
Turing's proofs relied on the concept of a universal Turing machine that can simulate any other Turing machine. He showed that if such a universal machine could solve the halting problem, it would lead to a logical contradiction. This demonstrated the inherent limitations of computation and formal systems.
Turing's work, along with Gödel's incompleteness theorems, established that there are true mathematical statements that cannot be proven within a formal system, and that the consistency of a sufficiently powerful formal system cannot be proven within the system itself.