Search existing math (mathlas index)
search_existing_mathSearch a 3.7M-document index to find known theorems and results for a given mathematical problem. Use source filters and weights to refine results.
Instructions
Find existing theorems/results for a problem from the mathlas 3.68M-doc index (dense + BM25 + RRF, fused with any live web_added findings). Use FIRST for any 'does known math solve this?' question; follow up with applicability_checklist on promising candidates. Args: query (problem/result description), k (default 10), optional corpus_dir (dataset parquets; omit to serve the prebuilt index or seed corpus), optional source_filter / source_weights to down-weight or exclude corpus sources, e.g. exclude web-mined docs when looking for canonical theorem statements.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| query | Yes | a problem / result description | |
| k | No | number of candidates (default 10) | |
| corpus_dir | No | optional dir of open theorem dataset parquets; omit to use the served index / built-in seed corpus | |
| source_filter | No | optional hard include/exclude of corpus sources, e.g. {"exclude": ["dolma"]} to drop web-mined docs when looking for canonical theorem statements. Keys: 'include' and/or 'exclude', values = lists drawn from arxiv / dolma / stacks / proofwiki / other. Default off (no behaviour change). | |
| source_weights | No | optional per-source score down-weighting, e.g. {"dolma": 0.5} to soft-demote web-mined docs (weight 0 = exclude). Source keys as in source_filter; weights >= 0 multiply the fused RRF score. Default off (no behaviour change). Note: down-weighting a source hurts queries whose true target IS that source — a per-query-intent knob, not a global default. |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| query | Yes | ||
| corpus | No | what was actually served | |
| k | No | ||
| live_findings_merged | No | ||
| candidates | Yes | ||
| next | No | ||
| note | No |