Since 1959, the International Mathematical Olympiad has included a total of 392 problems.
136 problems have been formalized (34.69%).
70 problems have complete formalized solutions (17.85%).