AIRI's LongTails AI agent proves 30 new math optimization theorems

Researchers at the AIRI Institute have successfully deployed an artificial intelligence agent named LongTails to prove more than 30 new theories in the field of mathematical optimization. The achievement was validated through rigorous checks by a formal verifier, marking a significant step forward in automating complex mathematical reasoning. This development opens new avenues for improving neural network training methods, enhancing logistics systems, and designing structures that balance lightness with durability.

Formal verification via Lean 4

The core advantage of the LongTails system lies in its reliance on automatic verification of every proof using the Lean 4 formal verification language. This mechanism addresses a persistent challenge in applying AI to mathematics: models often generate reasoning that appears convincing but contains hidden errors or solves the wrong problem. By starting from a formal description of conditions and objectives, the system ensures that each result undergoes official scrutiny confirming its validity, rather than relying solely on superficially correct inference.

Scientists at the AIRI Institute developed this open-source framework in collaboration with a colleague from Vietnam. According to the institute’s press service, as reported by science.mail, the AI agent can formulate new problems in mathematical optimization, propose solution methods, and then rigorously demonstrate the effectiveness of these approaches.

Nearly 100 theories formulated

Using the new framework, researchers managed to formally state approximately 100 theories. Among these, 50 improve upon guarantees found in previous studies, while the team plans to publish another 35 as independent mathematical results worthy of international dissemination. On average, the program requires between three and seven hours to prove a single theory.

Mathematical optimization focuses on identifying the best option from a vast set of possibilities, whether the goal is speed, cost reduction, accuracy, or reliability. The theories proven by the system clarify how quickly specific methods execute and under what conditions they operate. This insight helps determine the number of required computational operations in advance, eliminating the need for random algorithm testing.

Impact on AI and industry applications

Neural network training, ranging from recommendation systems to large language models, depends heavily on mathematical optimization techniques. Developing more efficient algorithms can reduce training time, lower computational costs, and decrease energy consumption within data centers, thereby improving the performance of systems reliant on these technologies.

The utility of these methods extends beyond artificial intelligence. They are applicable in designing lightweight yet strong structures, planning delivery routes, distributing power grid loads, discovering new molecules and materials, processing physical experiments, and managing investment risks.

Open source availability and future goals

The code for LongTails has been released as open source, allowing other research groups to utilize its capabilities for studying mathematical optimization problems and proving new theories. This accessibility facilitates the expansion of experimental scopes and the development of more complex methods for verifying algorithm efficiency.

One project participant noted that the framework achieved results in just a few days that surpassed their entire professional career output. While expressing difficulty in defining their emotional response to this advancement, the researcher described it as extremely exciting. The team intends to continue working on proving new theories, increasing the complexity and organization of problems, and verifying the practical application effectiveness of the algorithms they develop.