You also need to know that every integer can be divided into its prime factors, the prime numbers that serve as the building blocks for all numbers. For example, the prime factors of 21 are 3 and 7, while for 12 they are 2, 2 and 3. For 12, 2 appears twice in the list of prime factors, so we can also talk about distinct prime factors, meaning we only list each number once. The idea is that you translate each part of a mathematical proof into a machine-readable form, and then a computer checks that each step is logically correct. Things have moved on since then, as artificial intelligence has started being used in formalisation, but I think we are still a long, long way from Mochizuki’s work being true outside of Japan.