An artificial intelligence system has scanned thousands of mathematics papers, then selected 77 promising results for researchers to examine.
The system, called FAR, is not necessarily given a specific problem to solve. Instead, researchers indicate a field of study. FAR then searches the scientific literature for questions that remain open. A conjecture is precisely a mathematical statement believed to be true, but for which no accepted proof is yet available.
To understand the value of this approach, it helps to look at the usual work of a mathematician. Finding an interesting problem already takes a great deal of time. Checking a proposed proof can take even longer. FAR attempts to automate part of both stages, while leaving final validation to human specialists.
During a trial in combinatorics, a branch of mathematics that studies arrangements and discrete structures in particular, the system started with 51,110 papers. It identified 5,245 related to the field being studied. FAR extracted 6,453 conjectures or potentially open problems from them, then retained 4,717 after verifying their status.
Each selected problem then received an attempted solution. The system produced 1,050 answers presented as new. Other AI agents checked these proposals and accepted 598 of them. A final stage reduced this set to 77 results considered interesting enough to deserve mathematicians' attention.
This selection remains important because a proof produced by an AI does not become true simply because another program approves it. The authors themselves examined 15 results they considered particularly interesting. All were mathematically correct. However, one of them had already been obtained a few months earlier, without being found by the automated searches.
In other words, the system is used as much to decide where to devote time as it is to attempt proofs. Three independent checks are notably applied to results presented as new before the final selection.
For now, the experiment focuses on combinatorics, a field the authors know well enough to verify the results. The system could work with other collections of papers and other subjects.