Archerkattri/mathlas

Загружает найденный в вебе результат в рабочий корпус mathlas, чтобы search_existing_math сразу возвращал его (provenance 'web_added'; BM25 всегда - без загрузки модели; полный dense retrieval тоже, если передать dense_vec, встроенный в пространство обслуживаемого индекса). Используйте после веб-поиска согласно search_directive. Аргументы: statement, slogan, source, необязательный name, необязательный dense_vec.

Декомпозирует формулировку теоремы-кандидата на атомарные предусловия и заключение, чтобы вы могли проверить их одно за другим в контексте вашей задачи (выявляет ошибочные применения, например, использование теоремы для замкнутого интервала на открытом интервале). Используйте после поиска, прежде чем полагаться на какого-либо кандидата. Аргументы: candidate_statement (текст формулировки результата).

Выдвигает гипотезы о соотношениях для вещественной константы, в стиле Ramanujan-Machine: PSLQ по обширному базису и поиск по цепным дробям/рекуррентным соотношениям; каждый кандидат численно ПРОВЕРЕН до >= 25 цифр, но НЕ доказан (источник: 'conjectured_relation'). Используйте, когда identify_constant возвращает UNIDENTIFIED. Аргументы: value (десятичная строка, МНОГО цифр), max_terms (по умолчанию 16), cf_depth (по умолчанию 200).

Изолированная среда поиска программ (FunSearch): action='evaluate' оценивает ВАШУ программу на Python для problem_id ('cap_set' или 'online_bin_packing') в песочнице без сети/с таймаутом/с rlimit; action='register' сохраняет оценённую программу в БД MAP-Elites; action='status' возвращает лучшие программы и few-shot контекст для написания следующего варианта. Используйте для итеративной эволюции программ: ВЫ - генератор, mathlas - детерминированный оценщик. Аргументы: action, problem_id, затем program_src (evaluate/register), score + behavior (register), timeout_s (evaluate), top_k (status).

Безошибочно определяет замкнутую форму действительного числа: PSLQ + поиск по замкнутым формам, каждый кандидат независимо перепроверяется с точностью до 50+ знаков, в противном случае честно указывается UNIDENTIFIED. Используйте, когда у вас есть числовая константа и вы хотите узнать, что это ТАКОЕ. Args: value (десятичная строка, укажите МНОГО цифр, >16), optional basis (имена констант, например ['pi','e']).

Сопоставляет целочисленную последовательность с ЛОКАЛЬНОЙ копией OEIS по ТОЧНОМУ совпадению подряд идущих членов (без нечёткого сопоставления; честно возвращает UNDETERMINED, если файлы данных отсутствуют). Используется, когда у вас есть не менее 4 целочисленных членов и вы хотите получить именованную последовательность. Аргументы: terms (список целых чисел), max_results (по умолчанию 5).

Строит каркас «потребности<->гарантии» (структурированные вопросы + шаблон для заполнения) между вашей проблемой и кандидатным результатом. Используется, когда применимость неочевидна и вам нужна структура для оценки (оценка остаётся за вами). Аргументы: problem, candidate_statement.

Получает СТРУКТУРИРОВАННЫЙ план веб-поиска для задачи: строки запроса arXiv, подразделы/категории, конкретные результаты, которые нужно искать, и какие другие инструменты mathlas запускать; mathlas НЕ выполняет веб-запросов (ВЫ ищете, затем передаёте результаты обратно через add_finding). Используйте, когда локальный индекс не дал результата. Аргументы: problem (описание).

Находит существующие теоремы и результаты для задачи из индекса mathlas на 3,68 млн документов (dense + BM25 + RRF, объединяется с любыми свежими результатами web_added). Используйте в первую очередь для любого вопроса вида «известная математика решает это?»; затем вызывайте applicability_checklist для перспективных кандидатов. Аргументы: query (описание задачи или результата), k (по умолчанию 10), необязательный corpus_dir (parquet-файлы набора данных; пропустите, чтобы использовался предсобранный индекс или исходный корпус), необязательные source_filter / source_weights, чтобы уменьшить вес источников корпуса или исключить их. Например, исключите документы, извлечённые из веба, когда ищете канонические формулировки теорем.

Находит ОБЪЯВЛЕНИЯ mathlib (имя + тип) через публичные сервисы Loogle (запросы по шаблону или типу, например '?a * ?b = ?b * ?a') и LeanSearch (запросы на естественном языке); это ЕДИНСТВЕННЫЙ инструмент, который сам обращается в интернет. Честно сообщает 'service unavailable', если сервис недоступен (хотя при этом выдаётся кэшированный ответ на тот же запрос возрастом <= 7 дней, с явной пометкой 'cached' и указанием его возраста). Используйте, когда нужно формальное имя/тип результата в Lean, например перед написанием сниппета verify_formal. Аргументы: query, k (по умолчанию 10), backend ('auto'|'loogle'|'leansearch').

Запускает НАСТОЯЩЕЕ ядро Lean 4 (БЕЗ LLM). Два режима: (1) передайте lean (полный фрагмент, например 'example : 2 + 2 = 4 := rfl') для проверки типов как есть; (2) передайте proof для ПРОВЕРКИ ДОКАЗАТЕЛЬСТВА: тогда statement должен быть пропозицией Lean 4, а proof - вашим доказательством (терм или тактический блок 'by ...'); mathlas строит theorem _mathlas_check : <statement> := <proof>, и ядро возвращает proof_status VERIFIED_PROOF / REFUTED (в kernel_error содержится точная жалоба ядра, используйте её для исправления доказательства и повторного вызова) / UNDETERMINED (нет toolchain / таймаут / неразрешимый импорт, честно, никогда не подделывает). sorry/admit ОТКЛОНЯЮТСЯ. mathlas никогда не пишет доказательства, только проверяет их. Сначала найдите имена деклараций через search_formal_math. Аргументы: statement, lean?, proof?.

Проверяет с абсолютной надёжностью, что выражение в замкнутой форме равно числовому значению: независимо пересчитывает его в sympy с повышенной точностью и подтверждает результат только при совпадении >= 20 значащих цифр. Используйте перед утверждением любого числового тождества. Аргументы: value (строка десятичного числа), closed_form (например, 'pi**2/6', 'zeta(3)').