FAR System Mines Math Literature to Solve Open Conjectures

The Problem Is the Problem: Scaling Mathematical Discovery with AI — Xiaol.x

Xiaol.x

Because expert verification is scarcer than computational reasoning, scaling mathematical discovery requires filtering literature and prioritizing problems against explicit objectives rather than attempting isolated conjectures.

AI-assisted summary of The Problem Is the Problem: Scaling Mathematical Discovery with AI — original source. Check the original for full context.

Source published:

Key ideas

  • The FAR (Find, Attempt, Recommend) framework shifts AI-assisted mathematics from solving isolated, hand-picked conjectures to a literature-wide pipeline that automatically searches, attempts, and filters open problems across an entire research direction. (0:50)
  • In an empirical combinatorics pilot processing 51,110 mathematics papers, FAR distilled 4,717 apparently open problems into 77 machine-recommended artifacts, of which all 15 manually audited by domain experts were confirmed mathematically correct. (3:41)
  • Empirical testing reveals that optimal compute allocation depends strictly on the target objective: ranking candidate problems by success probability maximizes raw solution volume, but finding top-tier 'trophy' results requires pre-filtering for high importance. (8:50)
  • The pipeline produced a genuine mathematical refutation of a conjectured 2 - o(1) lower bound on independent set size ratios by generating a Cartesian product counterexample (C_5 × K_{m,m}) with an asymptotic ratio of 24/13 ≈ 1.846. (10:44)

Detailed notes

## Background Published on YouTube by channel Xiaol.x on August 26, 2026, this video examines the paper "The Problem Is the Problem: Towards Scalable Mathematical Discovery." It covers FAR (Find, Attempt, Recommend), a literature-to-review pipeline designed to scale AI-assisted mathematical research by sweeping literature for open conjectures, attempting solutions, and routing prioritized candidates to human experts.

## TL;DR As AI models become capable of attempting thousands of mathematical proofs, the primary bottleneck shifts from raw automated solving to managing scarce human review attention and deciding which problems merit computation. The FAR framework reconfigures discovery by taking a broad mathematical domain—demonstrated through a 51,110-paper combinatorics pilot—and running a search cascade that extracts, checks, attempts, and judges open conjectures down to a curated set of artifacts. By framing attempt allocation as a multi-armed bandit problem with submodular objectives, the system illustrates how prioritization heuristics change depending on whether the goal is volume or peak artifact importance. While concrete breakthroughs such as a graph-theoretic counterexample were validated, the findings emphasize that automated systems cannot replace human verification of correctness, authentic novelty, and conceptual meaning.

## Atmosphere & style The presentation carries the methodical, rigorous tone of a high-level computer science and mathematics seminar. Rather than hyping artificial intelligence breakthroughs, the exposition remains grounded and analytical, dissecting mathematical formulas, pipeline funnels, and submodular optimization with quiet precision. It feels clear-headed, scholarly, and deeply pragmatic, balancing genuine excitement over concrete mathematical counterexamples with steady caution regarding evaluation limits and the irreplaceable role of human oversight.

## Bulletin - [00:50](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=50s) The FAR (Find, Attempt, Recommend) framework shifts AI-assisted mathematics from solving isolated, hand-picked conjectures to a literature-wide pipeline that automatically searches, attempts, and filters open problems across an entire research direction. - [03:41](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=221s) In an empirical combinatorics pilot processing 51,110 mathematics papers, FAR distilled 4,717 apparently open problems into 77 machine-recommended artifacts, of which all 15 manually audited by domain experts were confirmed mathematically correct. - [08:50](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=530s) Empirical testing reveals that optimal compute allocation depends strictly on the target objective: ranking candidate problems by success probability maximizes raw solution volume, but finding top-tier 'trophy' results requires pre-filtering for high importance. - [10:44](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=644s) The pipeline produced a genuine mathematical refutation of a conjectured 2 - o(1) lower bound on independent set size ratios by generating a Cartesian product counterexample (C_5 × K_{m,m}) with an asymptotic ratio of 24/13 ≈ 1.846.

## Key takeaways - [00:00](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=0s) The primary bottleneck in automated mathematics has shifted from raw proof generation to attention allocation: computational reasoning is scarce, but expert human verification is even scarcer. - [00:50](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=50s) Rather than relying on human users to supply individual problems, FAR redraws the interaction boundary by allowing researchers to specify broad disciplines (such as combinatorics) while the system surfaces and filters candidate open problems. - [01:44](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=104s) FAR adopts a search-engine cascade architecture (Label, Extract, Check, Solve, Judge, Grade) that uses inexpensive, high-recall filtering early on before committing expensive reasoning compute to surviving candidates. - [02:42](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=162s) Candidate conjectures preserve full provenance—including origin papers, surrounding prose, and local notation—which is essential for downstream solvers to interpret problems correctly and for humans to audit claims. - [03:41](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=221s) From an initial corpus of 51,110 mathematics papers, the combinatorics pilot yielded 4,717 well-posed open problems, 1,050 single-attempt resolution claims, 598 multi-judge verified resolutions, and 77 recommended artifacts. - [04:52](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=292s) Pre-attempt heuristics for difficulty and importance achieved AUC ranking scores of 0.69 and 0.60 respectively, while exhibiting a 0.83 mutual correlation that reflects literature survival bias. - [06:57](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=417s) System allocation can target different mathematical objectives: artifact volume (F_1), cumulative importance (F_2), or the single best breakthrough artifact (F_3), which exhibits diminishing marginal returns as a monotone submodular set function. - [08:50](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=530s) Optimizing for peak artifact value (F_3) under tight compute budgets is best achieved by a two-stage heuristic that restricts attempts to the top 10% most important problems before sorting by estimated success probability. - [09:48](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=588s) Pipeline outputs demonstrate that correctness is distinct from novelty: audited resolutions included genuine novel discoveries, cross-domain applications of known constructions, and one valid proof whose precedent had already been published four months prior. - [10:44](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=644s) The pipeline cleanly refuted an independent set ratio lower bound of 2 - o(1) through a 10m-vertex graph construction whose maximum-to-average independent set ratio evaluates asymptotically to 24/13. - [11:48](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=708s) Key limitations of the pilot include an unmeasured end-to-end recall rate for missed open problems, budget metrics restricted strictly to solver calls, and a non-randomized human audit sample based on author interest. - [12:37](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=757s) FAR is designed not as an autonomous artificial mathematician, but as an attention architecture that sandwiches computational reasoning between human domain selection at the front and human validation at the end.

## Detailed walkthrough ### [00:00](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=0s) Proof Abundance and the Attention Scarcity Paradox

Even if an AI model tomorrow could effortlessly attempt a thousand mathematical conjectures before lunch, the mathematical enterprise would not suddenly become a thousand times easier. Instead, sheer automated scale creates two paralyzing bottlenecks on either side of the computation. At the entrance to the system, someone has to decide which problems actually merit those expensive attempts. At the exit, an expert must sift through piles of plausible-looking arguments to decide which proofs deserve an afternoon of human verification. While modern automated solvers sitting in the middle grow increasingly formidable, both surrounding queues threaten to expand without bound.

This tension defines the core premise of the paper: frontier model reasoning is scarce, but expert human attention is scarcer still. Consequently, the bottleneck in automated mathematics has shifted away from simply discovering how to prove a preselected, hand-picked conjecture. The real challenge is determining how to allocate both computational reasoning and human review across an entire discipline. As the authors frame it: "The problem is the problem."

[00:50](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=50s) Reimagining the Interface: Moving from Problem to Direction

Existing mathematical AI architectures operate on a point-to-point interface. In standard setups—such as FunSearch, AlphaEvolve, formal proof search systems, or autonomous problem-solving agents—a human researcher selects an isolated conjecture, feeds it to a solver, and then inspects the resulting output. While automated conjecturing takes an alternate route by inventing brand-new conjectures from scratch, the FAR (Find, Attempt, Recommend) framework explicitly rejects both paradigms as its primary contribution.

Instead of forcing a researcher to specify individual targets, FAR redraws the interaction boundary. The user provides a broad research direction—such as combinatorics—and hands over the search burden to the system. FAR scours the academic literature for author-stated open problems, executes attempts against them, and filters down the results into a compact, manageable queue designed for human verification. The existing solving apparatus remains vital, but target discovery and attention routing are elevated into first-class system components.

```mermaid flowchart TD accTitle: The FAR Literature to Review Pipeline accDescr: A cascade showing literature intake through filtering, solving, judging, and expert review. subgraph Intake["Literature Ingestion & Filtration"] A["51,110 Math Papers"] -->|"Label: Combinatorics"| B["5,245 Papers"] B -->|"Extract"| C["6,453 Candidate Problems"] C -->|"Check: Open & Well-Posed"| D["4,717 Target Conjectures"] end

subgraph Reasoning["Reasoning & Verification"] D -->|"Solve: 1 Attempt Each"| E["1,050 Claimed Resolutions"] E -->|"Judge: 3 Independent Passes"| F["598 Surviving Passes"] F -->|"Grade: Model Publishability"| G["77 Recommended Artifacts"] end

subgraph Review["Human Evaluation"] G -->|"Expert Selection"| H["15 Manually Reviewed (15 Correct)"] end ```

[01:44](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=104s) The FAR Search Cascade and Provenance

Rather than deploying a costly ranker over every raw document on the web, modern search engines run a multi-stage cascade: broad, cheap retrieval first, followed by heavier compute as candidates narrow. FAR applies this exact operational economics to the mathematical literature. The stages mirror a recommender funnel where the end user is an expert mathematician and the scarce good being recommended is high-value human attention:

1. **Label:** Restricts the corpus to papers belonging to the target mathematical discipline. 2. **Extract:** Surfaces concrete, unresolved statements from the text. 3. **Check:** Filters out statements that are ill-posed, unverified, or already solved in subsequent literature. 4. **Solve:** Dedicates the strongest reasoning compute to the surviving candidate pool. 5. **Judge and Grade:** Uses independent evaluator models to assess correctness and publishability before routing artifacts to human experts.

Academic literature is inherently messy; an unresolved problem might appear as an explicitly numbered conjecture, an informal remark in prose, a stubborn edge case, or a historical question settled long after initial publication. Because an extraction failure is fatal—if the extraction step misses a genuine problem, downstream stages can never recover it—early extraction is kept deliberately permissive. The checking stage then rigorously evaluates whether the statement remains truly open. Crucially, surviving candidates do not pass forward as isolated, decontextualized strings; each retains full provenance, including its source paper, original label, contextual notation, and surrounding historical status. In one pilot example involving a symmetric group character conjecture, this provenance enabled the solver to interpret the problem's local notation accurately and gave reviewers a paper trail to audit original author claims.

[03:41](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=221s) Tracing the Combinatorics Pilot Funnel

The empirical pilot paper demonstrates how dramatically the cascade compresses a vast literature into an actionable queue, running through a succession of measured stages:

- **51,110** total mathematics papers enter the system. - **5,245** combinatorics papers are retained after the domain labeling step. - **6,453** candidate statements and open problems are identified during permissive extraction. - **4,717** statements survive the checking phase as well-posed, apparently open problems. - **1,050** outcomes labeled as new solutions, claimed proofs, or counterexamples are produced after dedicating a single solving attempt per problem. - **598** potential resolutions survive an agreement check requiring approval from three independent model judges. - **77** artifacts are ultimately graded by the system as substantial enough to warrant publication. - **15** artifacts, selected from the 77 based on author interest, were subjected to rigorous manual human review.

All 15 manually audited artifacts proved to be mathematically correct. However, the distinction between machine recommendation and human verification is critical: the figure of 77 represents machine-recommended artifacts, not 77 certified mathematical breakthroughs.

[04:52](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=292s) Multi-Armed Bandits and Scoring Signals under Uncertainty

The pilot's search mechanics can be conceptualized as a multi-armed bandit problem, where each conjecture represents an arm and an expensive solving run represents a pull. Standard bandit algorithms dynamically balance exploration across uncertain arms against exploitation of the top-performing arms. The combinatorics pilot implements a simpler baseline: it pulls every single arm exactly once, mirroring the initialization step of an Upper Confidence Bound (UCB) algorithm rather than an adaptive policy.

To determine whether pre-attempt heuristics could guide pulls more effectively than uniform random selection under a restricted compute budget, the checking model assigns two separate scalar scores to each conjecture before any solver runs: - **Difficulty:** Calibrated on a scale from a basic exercise to a top-tier journal problem. - **Importance:** Calibrated on a scale from trivial mathematical content to a field-defining open question.

Following the full sweep, the predictive validity of these signals was evaluated using the Area Under the Receiver Operating Characteristic Curve (AUC): - The **Difficulty** dial attained an AUC of 0.69 when distinguishing problems where solving attempts yielded no accepted resolution. - The **Importance** dial reached an AUC of 0.60 when predicting whether a judge-passed resolution would be graded as publishable.

Importantly, AUC measures pairwise ranking consistency rather than absolute score calibration, meaning these signals are useful ranking heuristics rather than infallible oracles. The two scores also exhibit a strong mutual correlation of 0.83. This correlation reflects a natural selection pressure within mathematical literature: within a pool of unresolved problems, statements tend to remain open precisely because they are difficult.

[06:57](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=417s) Mathematical Objectives and Submodular Selection

Deciding which conjectures to prioritize depends entirely on the mathematical objective. Consider an illustrative dilemma: three conjecture cards sit on a board, but only two attempt tokens are available. Card A is easy but mathematically modest; Card B is profoundly important but nearly impossible; Card C offers a moderate probability of delivering a meaningful result. Choosing the optimal two cards requires formally defining what constitutes system success.

Let $S \subseteq P$ represent the chosen subset of conjectures drawn from the candidate pool $P$, and let $B$ denote the available attempt budget ($|S| = B$). The system chooses $S$ to maximize expected artifact value under one of three distinct objectives studied in the paper: - **$F_1$ (Artifact Count):** Maximizes the total number of successfully resolved artifacts. - **$F_2$ (Total Importance):** Maximizes the cumulative model-assigned importance across all resolved artifacts. - **$F_3$ (Single Best Artifact):** Maximizes the importance of the single highest-value artifact returned.

If the true success probability $P(C)$ of each conjecture were known, linearity of expectation makes $F_1$ and $F_2$ straightforward: optimizing $F_1$ simply requires ranking candidates by $P(C)$, while optimizing $F_2$ requires ranking by the product of importance and $P(C)$. However, the $F_3$ "trophy" objective behaves fundamentally differently. If an arm selection already yields a verified result with an importance score of 0.9, adding another result scored at 0.7 adds zero marginal value to the objective.

Because $F_3$ exhibits diminishing marginal returns, it forms a monotone submodular set function. Standard greedy approximation algorithms can achieve a theoretical $(1 - 1/e)$ approximation factor when exact marginal gains are known. However, calculating those gains requires knowing the joint probability distribution over candidate outcomes; individual per-item probabilities $P(C)$ are insufficient on their own.

[08:50](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=530s) Empirical Budget Allocation Strategies

Evaluating allocation strategies via five-fold cross-validation across the combinatorics pilot demonstrates that no single ranking method dominates across all objectives:

- **Maximizing Volume ($F_1$):** Ranking purely by estimated success probability consistently outperforms uniform random allocation across all tested budget limits. At a budget cap of 300 attempts, ranking by success probability yields an expected count of 7.92 resolved artifacts compared to 5.17 under uniform selection. - **Maximizing the Trophy Artifact ($F_3$):** Ranking the entire candidate pool solely by success probability fails as the budget expands, eventually falling behind uniform random selection because it systematically over-allocates attempts to easy, low-value exercises.

To overcome this, the most effective heuristic for $F_3$ applies a two-stage filter: it first isolates the top 10% of candidates by importance, and then ranks candidates within that elite subset by their estimated probability of success. At a tight budget of 50 attempts, this hybrid strategy secures an expected peak importance of 0.841, dramatically outperforming uniform selection's score of 0.299. The operational takeaway is clear: "The objective chooses the strategy."

[09:48](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=588s) Distinguishing Correctness, Novelty, and New Connections

A mathematically correct proof does not inherently represent a new discovery. The pilot explicitly dissects reviewed artifacts across three distinct categories:

1. **Known Results (Missed Precedent):** The pipeline generated a valid proof concerning a divisor difference problem and graded the finding as novel. However, subsequent human investigation revealed that the exact result had already been published four months prior, exposing a blind spot in the pipeline's novelty filtering. 2. **Novel Cross-Domain Connections:** The system imported a finite geometry construction that was already established in one area of mathematics and applied it to resolve a conjecture in another domain where the connection had not previously been recognized. 3. **Genuine Novel Discoveries:** Domain experts found no prior literature precedent for several reviewed outputs, including a complexity-theoretic proof, an answer establishing density one for a problem regarding binomial divisibility, and an explicit graph-theoretic counterexample.

These divergences demonstrate that mathematical correctness, novelty, and the creative bridging of disparate concepts represent fundamentally distinct judgments, all of which must be evaluated within a discovery pipeline.

[10:44](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=644s) Concrete Proof: Refuting the Independent Set Lower Bound

To ground the system's output in concrete mathematics rather than abstract workflow schematics, the paper details a specific graph-theoretic counterexample generated by the pipeline. The problem centered on a conjectured lower bound of $2 - o(1)$ on the ratio between the maximum and average independent set sizes for certain graphs.

The system refuted this bound by constructing the Cartesian product of a 5-cycle ($C_5$) and the complete bipartite graph $K_{m,m}$:

- **Fiber Structure:** Each vertex in $K_{m,m}$ is replaced by a 5-cycle pentagon fiber. Adjacent fibers are connected coordinate by coordinate, forcing independent sets selected across opposite bipartite partitions to occupy disjoint coordinate subsets of the pentagon. - **Graph Properties:** The resulting product graph is triangle-free, possesses $10m$ vertices, and has a uniform degree of $m + 2$. - **Set Invariants:** The graph's maximum independent set achieves a size of $4m$. - **Asymptotic Ratio:** Using a combinatorial counting argument, the average independent set size is shown to be asymptotically: $$\frac{13m}{6}$$ - **The Refutation:** Taking the ratio of maximum to average independent set size yields: $$\frac{4m}{\frac{13m}{6}} = \frac{24}{13} \approx 1.846$$ Because $1.846$ is strictly less than 2, the construction cleanly refutes the proposed $2 - o(1)$ lower bound while leaving weaker neighboring conjectures intact.

[11:48](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=708s) Limitations and FAR as Attention Architecture

To prevent overinterpreting the experimental findings, several key methodological constraints must be emphasized: - **No End-to-End Recall Metric:** The pipeline does not measure how many genuine open conjectures were missed during the early literature retrieval and extraction phases. - **Qualitative Capabilities:** Conceptual visualizations of the model's "reachable capability region" are purely illustrative abstractions rather than calibrated quantitative boundaries. - **Restricted Experimental Scope:** The empirical pilot was limited to a single combinatorics corpus, a uniform single-attempt budget per candidate problem, and a single underlying model stack. - **Narrow Budget Accounting:** The budget variable $B$ tallies only raw solver attempts, ignoring upstream token consumption, judging overhead, wall-clock inference time, and expert human review labor. - **Non-Random Human Audit:** The 15 manually verified artifacts were chosen based on the researchers' subjective topical interests rather than through a randomized sample of the 77 recommended candidates. - **Precedent Leakage:** As demonstrated by the divisor difference result, automated novelty grading remains imperfect and can fail to detect recent publications.

Ultimately, FAR is not presented as an autonomous artificial mathematician, but as a structured architecture for guiding mathematical attention. Its core contribution lies in establishing broad recall at the earliest literature stages, using coarse computational heuristics to triage open problems, and protecting the scarce time of human mathematicians.

[12:37](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=757s) Human Oversight in the Architecture of Mathematical Attention

The concluding architecture of the system balances automated reasoning with rigorous oversight by reserving "expensive skepticism late" and applying an explicit optimization objective to guide where compute and reasoning are directed. Rather than displacing human mathematicians, the framework repositions human effort where it matters most: people still define the research direction at the very start of the pipeline and retain full responsibility for evaluating meaning, determining true novelty, and providing final validation at the end.

```mermaid flowchart LR accTitle: Human-in-the-Loop Discovery Pipeline accDescr: Diagram illustrating human roles at the start and end of the automated reasoning pipeline.

subgraph Inputs["Inception"] H1["Human Direction & Scope"] end

subgraph Pipeline["FAR Automated Engine"] direction TB F1["Explicit Reasoning Objectives"] F2["Late-Stage Expensive Skepticism"] F1 --> F2 end

subgraph Outputs["Evaluation"] H2["Human Validation, Novelty & Meaning"] end

H1 --> Pipeline Pipeline --> H2 ```

- **Late-Stage Verification:** Computational skepticism and intensive scrutiny are deliberately concentrated late in the pipeline, ensuring deep evaluation is spent only on high-potential candidates. - **Explicit Objectives:** Mathematical reasoning is guided by a formal objective function rather than unconstrained exploration. - **Human Bookends:** The researcher initiates the process by selecting the mathematical domain and concludes it by certifying validity, contextual meaning, and authentic novelty.

## Notable quotes > [00:00](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=0s) The problem is the problem.

> [08:50](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=530s) The objective chooses the strategy.

> [00:00](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=0s) frontier model reasoning is scarce, but expert human attention is scarcer still.

> [06:57](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=417s) The system chooses S to maximize expected artifact value under one of three distinct objectives studied in the paper

> [03:41](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=221s) The figure of 77 represents machine-recommended artifacts, not 77 certified mathematical breakthroughs.

> [01:44](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=104s) Because an extraction failure is fatal—if the extraction step misses a genuine problem, downstream stages can never recover it—early extraction is kept deliberately permissive.

> [06:57](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=417s) Because F3 exhibits diminishing marginal returns, it forms a monotone submodular set function.

> [12:37](https://www.youtube.com/watch?v=MTHnSNVcWJo&t=757s) reserving 'expensive skepticism late' and applying an explicit optimization objective to guide where compute and reasoning are directed.

## Mentioned FAR (Find, Attempt, Recommend), FunSearch, AlphaEvolve, Xiaol.x, “The Problem Is the Problem: Towards Scalable Mathematical Discovery” (arXiv:2608.16977), Upper Confidence Bound (UCB), Area Under the Receiver Operating Characteristic Curve (AUC)

## Video description What happens when AI can attempt thousands of mathematical conjectures—but experts still have limited time to review the results?

This video explains FAR (Find, Attempt, Recommend), a literature-to-review pipeline designed to scale AI-assisted mathematical discovery. Instead of giving an AI system one conjecture at a time, researchers specify a direction—such as combinatorics—and FAR searches the literature, extracts open problems, attempts solutions, filters the results, and prioritizes artifacts for expert review.

The combinatorics pilot processes:

- 51,110 mathematics papers - 5,245 combinatorics papers - 6,453 candidate conjectures and open problems - 4,717 apparently open, well-posed problems - 598 model-judged potential resolutions - 77 machine-recommended artifacts - 15 manually reviewed results

The video also explores search cascades, bandit-style allocation, AUC score validity, submodular objectives, budget strategies, novelty versus correctness, and a concrete graph-theoretic counterexample.

Important caveat: 77 artifacts were machine-recommended, not 77 human-certified discoveries. Expert judgment remains essential for correctness, novelty, context, and validation.

Based on: “The Problem Is the Problem: Towards Scalable Mathematical Discovery” Paper: https://arxiv.org/abs/2608.16977

Chapters

00:00 Proof abundance creates attention scarcity 00:50 From choosing a problem to choosing a direction 01:44 FAR as a search cascade 02:42 Why conjectures need provenance 03:41 Reading the pilot funnel correctly 04:52 The bandit analogy 05:50 Difficulty and importance signals 06:57 Naming the optimization objective 07:55 Probability and submodular selection 08:50 Why the best strategy depends on the objective 09:48 Correctness, novelty, and new connections 10:44 A concrete graph counterexample 11:48 FAR as an architecture for mathematical attention

[Source](https://www.youtube.com/watch?v=MTHnSNVcWJo)

中文简报

FAR系统挖掘数学文献以解决公开猜想 由于专家验证比计算推理更为稀缺，扩展数学发现需要过滤文献并针对明确目标确定问题优先级，而非孤立地尝试单个猜想。 随着AI模型变得有能力尝试数千个数学证明，主要瓶颈已从单纯的自动化求解转向管理人力审查精力的稀缺性，并决定哪些问题值得投入计算。FAR框架重构了发现流程，它选取一个广泛的数学领域——通过一项包含51,110篇论文的组合学试点研究进行了展示——并运行一个级联搜索流程，对公开猜想进行提取、核查、尝试和评判，最终筛选出一套精选成果。通过将尝试资源的分配构建为具有次模目标的多臂老虎机问题，该系统阐释了优先级启发式策略如何根据目标是追求产出数量还是顶级成果重要性而发生改变。尽管系统验证了如图论反例等具体突破，但研究结果强调，自动化系统无法取代人类对正确性、真正新颖性以及概念意义的验证。 FAR（发现、尝试、推荐）框架将AI辅助数学研究从求解孤立、人工挑选的猜想，转变为面向整个文献的流程，能够在整个研究方向上自动搜索、尝试并过滤公开问题。 (0:50) 在一项处理了51,110篇数学论文的组合学实证试点中，FAR将4,717个看似公开的问题精简为77个机器推荐成果，其中由领域专家人工审核的全部15个成果均被确认在数学上是正确的。 (3:41) 实证测试表明，最佳算力分配严格取决于既定目标：按成功概率对候选问题进行排序可以最大化原始解题数量，但寻找顶尖“重磅”成果则需要预先筛选出高重要性的问题。 (8:50) 该流程对独立集大小比率猜想的 2 - o(1) 下界提出了真正的数学驳斥，生成了一个笛卡尔积反例 (C_5 × K_{m,m})，其渐近比率为 24/13 ≈ 1.846。 (10:44)

Reading summary

The core bottleneck in AI-driven mathematics is not generating candidate proofs for isolated conjectures, but allocating computational reasoning and scarce human attention across vast problem spaces. The authors propose the FAR (Find, Attempt, Recommend) framework to shift human interaction from point-to-point problem inputs to broad research directions, scouring the academic literature to curate actionable verification queues. The Attention Bottleneck and Direction-Based Discovery (0:00) As automated theorem solvers improve, scaling computation creates severe bottlenecks at both ends of the research workflow: deciding which open problems merit costly reasoning runs, and vetting machine-generated arguments before human mathematicians invest time in manual review. Frontier model reasoning remains computationally scarce, but expert human attention is scarcer still. Rather than relying on isolated conjecture solving or generating conjectures from scratch, the FAR framework accepts a broad disciplinary direction—such as combinatorics—and offloads the search burden to the system. By extracting author-stated open problems directly from the academic literature, executing resolution attempts, and filtering candidates into a compact queue, the framework repositions automated discovery from solving hand-picked problems to routing attention across an entire discipline. The Multi-Stage Literature Cascade (1:44) Operating like a search engine cascade, the pipeline applies a progressive sequence—Label, Extract, Check, Solve, Judge, and Grade—to prevent deploying expensive reasoning compute over raw text. Early extraction remains deliberately permissive to avoid fatal omissions of viable problems, while the checking phase filters out ill-posed, resolved, or unverified claims while preserving full provenance, such as original notation and surrounding publication context. In an empirical combinatorics pilot, the system ingested 51,110 mathematics papers, retaining 5,245 under domain labeling. Permissive extraction produced 6,453 candidate problems, of which 4,717 survived the checking phase as well-posed open conjectures. Dedicating a single solver attempt per conjecture yielded 1,050 claimed resolutions; 598 survived an agreement check across three independent model judges, and 77 were graded as publishable. Human experts manually audited 15 of these 77 artifacts based on topical interest, confirming all 15 were mathematically correct, though the authors emphasize that 77 represents machine recommendations rather than certified breakthroughs. Objective-Driven Allocation and Heuristic Scoring (6:57) The pilot models candidate exploration as a multi-armed bandit problem, testing pre-attempt scalar scores for Difficulty (AUC 0.69) and Importance (AUC 0.60) to guide problem selection under constrained attempt budgets. The two metrics exhibit a strong mutual correlation of 0.83, reflecting the empirical tendency of open problems in published literature to remain unsolved primarily because they are mathematically difficult. Budget allocation depends strictly on the governing mathematical objective. When maximizing the total count of resolved artifacts ($F_1$), ranking directly by estimated success probability consistently outperforms uniform random selection, delivering 7.92 resolved artifacts versus 5.17 under uniform selection at a 300-attempt budget. Conversely, maximizing the single best trophy artifact ($F_3$) acts as a monotone submodular set function with diminishing marginal returns. Because ranking solely by success probability over-allocates compute to easy, low-value exercises, the authors found the best heuristic for $F_3$ isolates the top 10% of candidates by importance before ranking by success probability, achieving an expected peak importance of 0.841 versus 0.299 for uniform selection at a 50-attempt budget. Correctness, Novelty, and Concrete Counterexamples (9:48) Mathematical validity does not inherently guarantee scientific novelty. Across audited artifacts, the pilot documented three categories: known results with missed precedent (a divisor difference proof that had already been published four months prior), novel cross-domain connections (importing a finite geometry construction to resolve a conjecture in another domain), and genuine novel discoveries, including a complexity-theoretic proof and a density-one result for binomial divisibility. To demonstrate concrete problem resolution, the pipeline refuted a conjectured lower bound of $2 - o(1)$ on the ratio between maximum and average independent set sizes. The system constructed a Cartesian product of a 5-cycle ($C_5$) and the complete bipartite graph $K_{m,m}$, producing a triangle-free graph with $10m$ vertices and degree $m + 2$. With a maximum independent set of $4m$ and an asymptotic average independent set size of $13m/6$, the ratio evaluated to $24/13 \approx 1.846$, strictly below 2 and disproving the conjectured bound. The authors emphasize that FAR functions as an attention-routing architecture rather than an autonomous artificial mathematician, leaving high-level research direction and final validation to human experts. Key methodological limitations include unmeasured end-to-end recall during early retrieval, a budget accounting metric that excludes upstream token and verification overhead, an evaluation restricted to 15 non-randomly selected artifacts, and vulnerability to literature blind spots where recent publications are missed.

Source quotes

[0:00] The problem is the problem. [8:50] The objective chooses the strategy. [0:00] frontier model reasoning is scarce, but expert human attention is scarcer still. [6:57] The system chooses S to maximize expected artifact value under one of three distinct objectives studied in the paper [3:41] The figure of 77 represents machine-recommended artifacts, not 77 certified mathematical breakthroughs. [1:44] Because an extraction failure is fatal—if the extraction step misses a genuine problem, downstream stages can never recover it—early extraction is kept deliberately permissive. [6:57] Because F3 exhibits diminishing marginal returns, it forms a monotone submodular set function. [12:37] reserving 'expensive skepticism late' and applying an explicit optimization objective to guide where compute and reasoning are directed.

Original transcript

[0:01] Suppose tomorrow's model can attempt a [0:03] thousand conjectures before lunch. [0:05] Mathematics does not become a thousand [0:07] times easier. It creates two queues. At [0:10] the entrance, someone must decide which [0:13] problems deserved those attempts. At the [0:16] exit, someone must decide which [0:18] plausible proofs deserve a [0:20] mathematician's afternoon. [0:22] The familiar solver in the middle may be [0:24] brilliant, yet both queues can still [0:26] grow without bound. This paper begins [0:29] with that paradox. Frontier model [0:32] reasoning is scarce. Expert mathematical [0:35] review is scarcer. So, the problem is no [0:38] longer only how to solve a chosen [0:40] conjecture. It is how to allocate [0:43] reasoning and review across a whole [0:46] research direction. [0:48] The problem is the problem. [0:50] The paper's first figure shows the [0:52] interface change. Above the line, a [0:55] mathematician chooses one conjecture, a [0:58] model attempts it, and an expert checks [1:00] the resolution. Systems such as [1:02] FunSearch, [1:04] Alpha Evolve, Formal Proof Search, and [1:07] autonomous problem-solving pipelines [1:09] already strengthen the middle of that [1:11] path. Automated conjecturing takes a [1:14] different route and creates new [1:16] conjectures. [1:18] FAR does neither of those as its main [1:20] contribution. [1:22] Below the line, the mathematician names [1:25] a direction such as combinatorics. [1:28] The system searches the literature for [1:30] author-stated open problems, attempts [1:32] them, and returns a small review queue. [1:35] The old solver remains useful. The [1:37] novelty is that target discovery and [1:40] attention routing become first-class [1:42] parts of the system. [1:45] A search engine does not run its most [1:47] expensive ranker over every item on the [1:49] internet. It begins with broad cheap [1:51] recall, then spends more computation as [1:54] the candidate set shrinks. FAR transfers [1:57] that economics to mathematics. The [2:01] paper's upper row is a recommender [2:03] cascade. The lower row is the [2:06] mathematical analog. [2:08] Label keeps papers in the chosen [2:10] direction. Extract recovers concrete [2:13] unresolved statements. Check removes [2:16] candidates that appear solved or [2:19] invalid. Solve spends the strongest [2:22] reasoning on the remaining pool. Judge [2:24] and grade decide what enters the [2:26] expert-facing queue. This is an [2:28] architectural analogy, not a claim about [2:31] clicks or personalization. [2:33] The user here is a mathematician [2:37] and the scarce item being recommended is [2:39] worthy expert attention. [2:43] Research literature is not a clean [2:45] benchmark table. [2:47] A live problem may be a numbered [2:48] conjecture, a question in prose, an [2:51] unresolved case, or a statement whose [2:53] status changed after publication. That [2:57] makes the early filters asymmetric. If [3:02] extract misses a real problem, no later [3:05] stage can recover it. So, extraction is [3:08] deliberately permissive. [3:10] Check then asks whether the text states [3:12] a concrete problem and whether credible [3:15] later work resolves it. The surviving [3:18] candidate is not just one sentence. It [3:20] carries the source paper, the original [3:23] label, local notation, and status [3:26] evidence. [3:27] The paper's example records a symmetric [3:30] group character conjecture this way. [3:33] That provenance lets the solver [3:35] interpret the target correctly and lets [3:37] a human later audit what the source [3:39] actually claimed. [3:42] Now, we can read the pilot without [3:45] inflating any number. The corpus [3:47] contains 51,110 [3:52] mathematics papers. Label keeps 5,245 [3:58] combinatorics papers. Extract finds [4:01] 6,453 [4:03] candidate statements. [4:05] Check leaves 4,717. [4:09] Apparently open well-posed problems. One [4:13] attempt per problem produces 1,050 [4:18] outcomes labeled new, claimed proofs, or [4:22] examples. [4:23] Three independent model judges must all [4:26] pass an outcome. [4:28] 598 survive. A later model grade calls [4:32] 77 substantial enough to publish. [4:35] Finally, the authors choose 15 that [4:38] interest them and manually review those [4:40] 15. All 15 are mathematically correct. [4:44] 77 means machine-recommended artifacts. [4:48] It does not mean 77 human-certified [4:50] discoveries. [4:53] The next pressure is allocation under [4:55] uncertainty. [4:57] Think of each conjecture as a bandit arm [5:00] and one expensive solving run as a pull. [5:02] A classical bandit repeats pulls, [5:05] balancing exploration of uncertain arms [5:08] with exploitation of the arms that [5:10] currently look best. This pilot does [5:12] something simpler. It pulls every arm [5:15] exactly once. That resembles only the [5:17] initialization phase of UCB, not a full [5:21] adaptive bandit algorithm. The paper's [5:23] reachable region figure gives the [5:25] intuition. Some problems sit inside the [5:28] current model's capability. Others may [5:31] become reachable only as models improve. [5:34] But, the figure is explicitly [5:37] illustrative and both axes are [5:39] qualitative. The measured question comes [5:42] later. With a smaller fixed budget, can [5:45] pre-attempt scores route pulls better [5:48] than uniform selection. [5:51] Before any solving, the checking model [5:53] assigns two dials. Difficulty runs from [5:57] an unpublishable exercise to a top [6:00] journal-level problem. Importance runs [6:03] from no substantive content to a [6:05] field-defining question. After the full [6:09] sweep, the outcomes let us test whether [6:11] those dials rank anything real. [6:14] Difficulty reaches an AUC of 0.69 for [6:18] separating attempts with no accepted [6:20] resolution. Importance reaches 0.60 [6:25] for separating model-judged passes that [6:28] the grader calls publishable. [6:30] AUC is a pairwise ranking probability, [6:34] not calibration, and not proof of [6:36] correctness. The two scores also [6:40] correlate at 0.83. [6:43] That selection effect makes sense. [6:46] Inside a pool of still open problems, [6:48] important questions often survive [6:50] precisely because they are hard. Useful [6:53] signals, yes. Oracles, no. [6:57] Put three conjecture cards on the board [6:59] and give us only two attempt tokens. [7:02] One card looks easy but modest. One [7:05] looks important but nearly impossible. [7:08] One offers a medium chance of a [7:10] meaningful artifact. [7:12] Which two should we attempt? The [7:14] question is incomplete until we name [7:16] success. [7:18] Let S be the selected subset of the [7:20] attemptable pool P, and let B be the [7:23] number of available attempts. We choose [7:26] S of size B to maximize the expected [7:30] value of the artifacts return from S. Um [7:33] the paper studies three values. F1 [7:37] counts artifacts. F2 sums their [7:40] model-scored importance. F3 keeps only [7:44] the importance of the single best [7:46] artifact. The same candidates and the [7:50] same budget can produce three different [7:53] rational allocations. [7:56] Now, the board has enough objects for [7:57] the probability equation. For conjecture [8:00] C, let P of C be the chance that one [8:02] attempt both survives judging and is [8:04] graded publishable. If the true [8:06] probabilities were known, linearity of [8:09] expectation makes the first two [8:11] objectives simple. To maximize artifact [8:14] count, rank by P. To maximize total [8:17] importance, rank by importance times P. [8:20] The best single artifact objective [8:22] behaves differently. Once the set [8:24] already contains a successful item of [8:26] importance 0.9, adding a possible 0.7 [8:30] result cannot improve the trophy. That [8:33] is diminishing returns. [8:35] The expected best value is monotone [8:37] submodular, so classical greedy [8:39] selection achieves 1 - 1 over E when its [8:42] true marginal gains are available. But [8:44] those gains depend on the joint outcome [8:46] distribution. Per item P alone is not [8:49] enough. [8:51] The paper's budget curves are the [8:52] empirical receipt evaluated by five-fold [8:55] cross-validation inside this one pilot [8:58] run. Read one panel at a time. For [9:01] artifact count, ranking on estimated [9:03] success probability beats uniform [9:05] selection at every tested budget. At [9:08] budget 300, the expected count rises [9:11] from about 5.17 [9:13] to 7.92. [9:15] But the right panel asks for the [9:17] importance of the single best artifact. [9:19] There, ranking the whole pool by success [9:22] eventually falls behind uniform [9:23] selection. The strongest tested [9:25] heuristic first keeps only the top 10th [9:28] by importance, then ranks by estimated [9:30] success inside that restricted set. At [9:33] budget 50, it reaches is 0.841 [9:37] versus 0.299 [9:39] for uniform. There is no universally [9:43] best ranking. The objective chooses the [9:46] strategy. [9:47] Uh a correct proof is not automatically [9:50] a new discovery, so the paper separates [9:52] three cases. In the first, the cascade [9:55] returns a correct divisor difference [9:57] result and grades it new, but the [10:00] authors find that the same statement had [10:02] been recorded 4 months earlier. The [10:05] novelty search missed it. In the second, [10:08] a finite geometry construction was known [10:11] in another context, but the system [10:13] connected it to a conjecture where that [10:15] link had not been made. In the third [10:18] group, the authors and domain experts [10:21] found no precedent for several reviewed [10:23] results. A complexity theoretic proof, a [10:27] graph counterexample, [10:29] and a density one answer [10:33] about binomial divisibility. [10:35] Correctness, novelty, and a new [10:37] connection are different mathematical [10:39] judgments. [10:40] A professional review pipeline must ask [10:42] all three. [10:45] Let us inspect one mathematical receipt [10:47] instead of ending on workflow boxes. [10:50] Take the Cartesian product of a five [10:52] cycle and the complete bipartite graph [10:55] KMM. [10:57] Each vertex of KMM carries a pentagon [11:00] fiber. Adjacent fibers are joined [11:03] coordinate by coordinate, so independent [11:05] sets chosen on opposite sides must use [11:08] disjoint parts of the pentagon. The [11:10] resulting graph is triangle-free, has [11:13] 10M vertices, and degree M + 2. Its [11:17] maximum independent set has size 4M. [11:20] A counting argument gives average [11:22] independent set size asymptotic to 13M [11:26] over 6. Therefore, the ratio of maximum [11:29] to average tends to [11:32] 24 over 13 about 1.846 [11:36] strictly below two. [11:38] That refutes the proposed [11:41] two minus little O lower bound while [11:44] leaving weaker nearby conjectures [11:46] untouched. [11:48] Um, return to the whole funnel and keep [11:51] the red boundaries visible. [11:54] There is no end-to-end recall estimate [11:56] for papers or conjectures missed [11:58] upstream. [12:00] The reachable region picture is [12:01] qualitative. The allocation study uses [12:05] one realized attempt per problem, one [12:08] combinatorics corpus, and one model [12:11] stack. Budget B counts solving attempts, [12:14] not all search, judging token wall time [12:17] or expert review cost. The 15 reviewed [12:20] artifacts were chosen by author [12:22] interest, not as a random audit of all [12:24] 77, and one correct result was already [12:27] known. [12:28] The durable contribution is therefore [12:31] bounded but important. Scalable [12:33] discovery needs broad recall early, [12:37] expensive skepticism late, and an [12:39] explicit objective for where reasoning [12:43] goes. Humans still choose the direction [12:45] at the beginning and remain responsible [12:47] for meaning, novelty, and validation at [12:49] the end.