Russian Mathematicians Teach AI Agents to Prove Theorems
Russian mathematicians, together with their Vietnamese colleagues, have created a system with which AI agents have proved more than 30 new theorems.
According to a statement from the press service of the AIRI Artificial Intelligence Institute, the system allows agents to formulate mathematical optimization problems and rigorously prove results. It is compatible with various AI agents and automatically verifies proofs by composing algorithms in the Lean language. This rules out convincing but erroneous solutions.
In total, the scientists worked through around one hundred theorems. For half of them, the guarantees known from previous work were improved, and 35 results are planned for publication. On average, an agent needs 3 to 7 hours to prove a single theorem.
