Since 1959, the International Mathematical Olympiad has included a total of 404 problems.
274 problems have been formalized (67.82%).
270 problems have complete formalized solutions (66.83%).