The development of mathematics towards greater precision has led to the formalization of many areas, where proofs can be carried out according to a few mechanical rules. The most comprehensive formal systems are the Principia Mathematica (PM) and the Zermelo-Fraenkel set theory (with von Neumann's extensions). These systems are so extensive that all currently used proof methods in mathematics can be formalized within them, based on a few axioms and rules. However, it is shown that this is not the case; there are simple problems in the theory of ordinary whole numbers that cannot be decided by the axioms of these systems. This is not due to the specific nature of these systems, but applies to a wide class of formal systems, including those that can be obtained by adding a finite number of axioms to the two mentioned systems, provided the added axioms do not allow the proof of false sentences of the type mentioned. We briefly outline the main idea of the proof. In a formal system (e.g., PM), formulas are finite sequences of basic symbols, and it is possible to precisely define which sequences are meaningful formulas. Similarly, proofs are finite sequences of formulas. For metamathematical considerations, it is irrelevant which symbols are used as basic symbols, so we choose natural numbers. A formula is then a finite sequence of natural numbers, and a proof is a finite sequence of such sequences. Metamathematical concepts (such as "formula," "proof," "provable formula") become concepts over natural numbers or sequences of such numbers and can thus be expressed in the symbols of PM. In particular, it is possible to define within PM a formula F(v) with a free variable v (of the type of a sequence of numbers), such that F(v) expresses that v is a provable formula. An undecidable sentence of PM is then constructed as a sentence A for which neither A nor not A is provable.The development of mathematics towards greater precision has led to the formalization of many areas, where proofs can be carried out according to a few mechanical rules. The most comprehensive formal systems are the Principia Mathematica (PM) and the Zermelo-Fraenkel set theory (with von Neumann's extensions). These systems are so extensive that all currently used proof methods in mathematics can be formalized within them, based on a few axioms and rules. However, it is shown that this is not the case; there are simple problems in the theory of ordinary whole numbers that cannot be decided by the axioms of these systems. This is not due to the specific nature of these systems, but applies to a wide class of formal systems, including those that can be obtained by adding a finite number of axioms to the two mentioned systems, provided the added axioms do not allow the proof of false sentences of the type mentioned. We briefly outline the main idea of the proof. In a formal system (e.g., PM), formulas are finite sequences of basic symbols, and it is possible to precisely define which sequences are meaningful formulas. Similarly, proofs are finite sequences of formulas. For metamathematical considerations, it is irrelevant which symbols are used as basic symbols, so we choose natural numbers. A formula is then a finite sequence of natural numbers, and a proof is a finite sequence of such sequences. Metamathematical concepts (such as "formula," "proof," "provable formula") become concepts over natural numbers or sequences of such numbers and can thus be expressed in the symbols of PM. In particular, it is possible to define within PM a formula F(v) with a free variable v (of the type of a sequence of numbers), such that F(v) expresses that v is a provable formula. An undecidable sentence of PM is then constructed as a sentence A for which neither A nor not A is provable.