The organizers of the International Mathematical Olympiad have proposed adding to its program a competition for the development of artificial intelligence capable of solving classical mathematical olympiad problems. The algorithm should be written in Lean.

International Mathematical Olympiad - World Championship in mathematics among high school students, held every year in one of the countries. The first MMO was held in 1959 in Romania with the participation of seven countries. In recent years, more than 100 countries from 5 continents participate in IMO. The IMO Council approves the host country of the IMO, monitors compliance with the rules and maintains the traditions of IMO.

Students must solve all the problems on their own, without using software - however, now the organizing committee intends to add a competition for the development of computer methods for solving problems.

Students to participate in the new competition will have to post the algorithm in open access, and a day before the start of the Olympiad send it to the organizing committee. The algorithm should work without the Internet - it will be given as much time to solve problems as other participants in the competition: 4.5 hours for each set of three tasks.

Previously, Libratus artificial intelligence, developed by engineers from Carnegie Melon University, defeated the six world poker champions who played at the same table.

hightech.fm