Since 1959, the International Mathematical Olympiad has included a total of 398 problems.
169 problems have been formalized (42.46%).
132 problems have complete formalized solutions (33.16%).