Since 1959, the International Mathematical Olympiad has included a total of 392 problems.
150 problems have been formalized (38.26%).
98 problems have complete formalized solutions (25.00%).