CMU's FAR system mines 5,245 math papers to surface 77 discoveries
AI pipeline turns literature search into a discovery engine for open conjectures.
The bottleneck in AI-assisted mathematics is no longer reasoning power but allocating scarce human attention. A new paper from Carnegie Mellon researchers (Zeyu Zheng, Shengtong Zhang, Jeremy Avigad, Prasad Tetali, and Sean Welleck) argues that current workflows waste expert review on poorly chosen problems. Their solution, FAR (Find, Attempt, Recommend), shifts human input from picking a single problem to specifying a research direction, letting the AI search literature for candidate problems, attempt them, and recommend only the most promising results.
In a combinatorics pilot, FAR scanned 5,245 papers, extracted 6,453 conjectures or open problems, and used automated filtering to keep 4,717 that were well-posed and still unresolved. After reasoning and triage, it surfaced 598 potential resolutions, narrowing to 77 for author-team review. These included breakthroughs on conjectures by Davies–Jenssen–Perkins–Roberts, Erdős–Straus, Ikenmeyer–Pak–Panova, and Lund–Saraf–Wolf. The results show a new mode of collaboration where AI accelerates the entire discovery loop—not just solving problems, but finding which problems are worth solving.
- FAR automates problem discovery: scans 5,245 papers, recovers 6,453 conjectures, filters to 4,717 open problems
- Pipeline surfaces 598 potential resolutions, with 77 selected for expert human review
- Found new results on conjectures by Erdős–Straus, Davies–Jenssen–Perkins–Roberts, and Ikenmeyer–Pak–Panova
Why It Matters
This shifts AI-for-math from problem-solving to problem-finding, letting researchers focus attention on the highest-value open questions.