Ramón López de Mántaras
Computer scientist and physicist, emeritus research professor at CSIC and pioneer of AI research in Spain
This is an excellent result. It demonstrates that mathematical problems formalizable through reinforcement learning (combined with other techniques, such as an interactive theorem prover and a powerful search algorithm to explore the space of possible proofs) are becoming accessible to AI, although it is important to note that they require considerable human expertise for their formalization and enormous computational power.
There are also other significant limitations. AlphaProof's specific learning phase requires a specialized and costly level of training. Solving the most difficult problems can take several days of inference, highlighting the need for more efficient strategies.
So far, the system's successes have been primarily in advanced secondary and undergraduate mathematics, which operates within a known and relatively fixed set of concepts. Extending these capabilities to advanced mathematical research, which involves theory building and the incorporation of new concepts, remains a monumental challenge, and there is no indication that it can be achieved in the short term, or even the medium term. In other words, these achievements do not mean that AI is comparable to a mathematician, since it does not 'understand' mathematical concepts at all, nor can it create solutions to entirely new problems. What AlphaProof demonstrates is a remarkable expansion of the automated tools that can assist human mathematicians, but never replace them. Nevertheless, it is reasonable to expect that AlphaProof will become a valuable tool for human researchers in the long term, opening new possibilities for exploring the limits of knowledge, but always as a tool that will only be useful to those with a deep understanding of mathematics.
The high computational requirements also raise concerns about the reproducibility and accessibility of this type of advancement, which is a serious handicap in science. That is why the developers of AlphaProof plan to create interactive tools for accessing this system and also aim to improve algorithmic efficiency, reducing barriers to entry and transforming these techniques into collaborative resources for the mathematical community.