Since 1959, the International Mathematical Olympiad has included a total of 398 problems.
156 problems have been formalized (39.19%).
108 problems have complete formalized solutions (27.13%).