∴ Библиотека решений
Решение
Уравнения прикладной математики из бенчмарка PolyaninBench, которые агент IMV решал на открытой модели gpt-oss-20b. Для каждой задачи — постановка (текст и Lean 4), найденные семейства решений, граф хода решения с формальными проверками и вывод о полноте. Вердикты выставил LLM-судья эксперимента IMV-2026; оценки людей появятся позже.
59 задач · gpt-oss-20b · найдено хотя бы одно семейство решений справочника — 49 · полнота доказана — 3 (из них подтверждена в Lean — 1) · по заключениям судьи
Что означают статусы и метки
- Решена полностью
- Найдены все семейства решений справочника, и доказан вывод о полноте, совпадающий с эталоном.
- Найдены все известные решения
- Найдены все семейства решений справочника; вопрос о полноте не закрыт.
- Решена частично
- Найдена часть семейств решений справочника.
- Не решена
- Ни одно семейство решений справочника не найдено.
- Найдено семейств: k / n
- Сколько из n семейств решений справочника агент нашёл — по итоговому заключению LLM-судьи (разные формы одного семейства судья считает одним). Тексты эталонов не публикуются.
- Судья
- Вердикт LLM-судьи о полноте: доказана, доказана неполнота, решения подтверждены (без вывода о полноте) или полнота не установлена. У большинства задач полнота не установлена и в самом справочнике.
- Полнота: Lean ✓
- Судья признал полноту доказанной, и формальная часть вывода о полноте проверена в Lean 4. Если Lean-код узла полноты компилируется, но судья полноту не признал, метки нет — это отмечено в отчёте задачи.
- Ход решения
- Качественная оценка всего прогона из итогового разбора эксперимента IMV-2026 — не только ответа, но и того, как агент к нему шёл: глубина поиска, корректность выкладок, подкрепление в Lean, отсутствие ложных «новых» решений. Шкала: сильный, средний, слабый, провал.
- Lean: k / m
- Сколько формальных фрагментов прошли проверку Lean 4 (на странице задачи). Компиляция не означает, что доказана теорема именно об условии задачи.
Алгебраические уравнения
eq01
\[(a - x^2)^3 = (b - x^3)^2\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: сильный
eq02
\[(x^3 + a)^3 + a = x\]
mo873.pdf: пример 7, уравнение (33)
Решена полностью
Найдено семейств: 1 / 1
Судья: Полнота доказана
Полнота: Lean ✓
Ход решения: сильный
eq03
\[(x^3 + x + b)^3 + x^3 + 2b = 0\]
mo873.pdf: пример 9, форма (38) при \(f(x) = x^3,\ a = 1\)
Решена полностью
Найдено семейств: 1 / 1
Судья: Полнота доказана
Ход решения: сильный
eq04
\[2z^6 - 3\alpha z^4 - 2\beta z^3 + 3\alpha^2 z^2 + \beta^2 - \alpha^3 = 0\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: сильный
eq05
\[x^5 - (a^4 - 3a^2 b + b^2)\,x + ab\,(a^2 - 2b) = 0\]
Решена полностью
Найдено семейств: 2 / 2
Судья: Полнота доказана
Ход решения: сильный
Функциональные уравнения
eq06
\[y(x)\,y(x+1) + a\,\bigl[y(x+1) - y(x)\bigr] = 0\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Полнота не установлена
Ход решения: сильный
eq07
\[y(\sin x) - y(\cos x) = 0\]
Найдены все известные решения
Найдено семейств: 2 / 2
Судья: Решения подтверждены
Ход решения: средний
eq08
\[y(x)\,y(a - x) = b^2\]
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: сильный
eq09
\[f(x+y) + f(x-y) = 2f(x) + 2f(y)\]
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: сильный
eq10
\[f(x, y) = a^n f\bigl(x + (1-a)\,y,\ a y\bigr)\]
Найдены все известные решения
Найдено семейств: 2 / 2
Судья: Решения подтверждены
Ход решения: средний
eq11
\[f(x+y) = f(x) + f(y) - a\,f(x)\,f(y)\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: слабый
eq12
\[\sqrt{\frac{f(x)^2 + f(y)^2}{2}} = f\Bigl(\sqrt{\frac{x^2 + y^2}{2}}\Bigr)\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: сильный
eq13
\[f(x+y) = g(x) + f(y) - f(x)\,h(y)\]
Найдены все известные решения
Найдено семейств: 2 / 2
Судья: Полнота не установлена
Ход решения: сильный
eq14
\[\begin{aligned} &f(t) + g(x)\,Q(z) + h(x)\,R(z) = 0,\\ &z = \varphi(x) + \psi(t) \end{aligned}\]
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: слабый
Интегральные уравнения
eq15
\[\int_0^x \frac{y(t)}{\sqrt{x - t}}\,dt = f(x)\]
интегральное уравнение Абеля 1-го рода
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: средний
eq16
\[\int_0^x \cosh\bigl[a(x - t)\bigr]\,y(t)\,dt = f(x)\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: сильный
eq17
\[\int_0^x \bigl\{\cosh\bigl[a(x - t)\bigr] + b\bigr\}\,y(t)\,dt = f(x)\]
Решена частично
Найдено семейств: 1 / 2
Судья: Полнота не установлена
Ход решения: средний
eq18
\[\int_0^x y(t)\,y(x - t)\,dt = ax + b\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: сильный
eq19
\[y(x) + a\int_0^x (x - t)\,y(t)\,dt = f(x)\]
Решена частично
Найдено семейств: 1 / 2
Судья: Полнота не установлена
Ход решения: сильный
eq20
\[a\,y(x) + \int_0^x y(t)\,y(x - t)\,dt = bx\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: сильный
eq21
\[\int_{-\infty}^{\infty} e^{-\lambda|x - t|}\,y(t)\,dt = f(x)\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: слабый
eq22
\[\int_{-\infty}^{\infty} \sin\bigl(\lambda|x - t|\bigr)\,y(t)\,dt = f(x)\]
Не решена
Найдено семейств: 0 / 1
Судья: Полнота не установлена
Ход решения: слабый
eq23
\[y(x) + \lambda\int_0^{\infty} e^{-|x - t|}\,y(t)\,dt = f(x)\]
уравнение Винера–Хопфа 2-го рода
Не решена
Найдено семейств: 0 / 2
Судья: Полнота не установлена
Ход решения: слабый
eq24
\[y(x) - \lambda\int_{-\infty}^{\infty} e^{-|x - t|}\,y(t)\,dt = 0\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: средний
eq25
\[y(x) - \lambda\int_0^{\infty} \sin(xt)\,y(t)\,dt = f(x)\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: сильный
eq26
\[y(x) + \int_a^b g(t)\,y(x)\,y(t)\,dt = f(x)\]
Не решена
Найдено семейств: 0 / 1
Судья: Решения подтверждены
Ход решения: средний
Обыкновенные дифференциальные уравнения
eq27
\[y'' + f(x)\,y' + a\bigl[f(x) - a\bigr]\,y = 0\]
Найдены все известные решения
Найдено семейств: 2 / 2
Судья: Решения подтверждены
Ход решения: сильный
eq28
\[x\,y'' + \bigl[x f(x) + a\bigr]\,y' + (a - 1)\,f(x)\,y = 0\]
Не решена
Найдено семейств: 0 / 2
Судья: Решения подтверждены
Ход решения: слабый
eq29
\[\begin{aligned} &x\,y'' + \bigl[(ax + 1)\,f(x) + ax - 1\bigr]\,y'\\ &\qquad + a^2 x\,f(x)\,y = 0 \end{aligned}\]
Не решена
Найдено семейств: 0 / 2
Судья: Полнота не установлена
Ход решения: слабый
eq30
\[x^4\,y'' + (ax^2 + bx + c)\,y = 0\]
Решена частично
Найдено семейств: 1 / 2
Судья: Полнота не установлена
Ход решения: сильный
eq31
\[(ax^2 + bx + c)^2\,y'' + y = 0\]
Не решена
Найдено семейств: 0 / 1
Судья: Полнота не установлена
Ход решения: средний
eq32
\[y\,y' - y = ax + b\]
уравнение Абеля 2-го рода
Решена частично
Найдено семейств: 1 / 2
Судья: Полнота не установлена
Ход решения: средний
eq33
\[y\,y' - y = ax + b\,e^{-2x/a}\]
уравнение Абеля 2-го рода
Не решена
Найдено семейств: 0 / 1
Судья: Полнота не установлена
Ход решения: слабый
eq34
\[y\,y'' - (y')^2 = a\,y^3 e^{\lambda x}\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: сильный
eq35
\[y'' = a\,y' + e^{2ax} f(y)\]
нелинейное автономно-усиленное
Найдены все известные решения
Найдено семейств: 2 / 2
Судья: Решения подтверждены
Ход решения: средний
eq36
\[y'' = \bigl[e^{ax} f(y) + a\bigr]\,y'\]
Найдены все известные решения
Найдено семейств: 2 / 2
Судья: Решения подтверждены
Ход решения: средний
eq37
\[y'' - a\,(y')^2 = f(x)\,e^{ay}\]
Найдены все известные решения
Найдено семейств: 1 / 1
Судья: Решения подтверждены
Ход решения: сильный
eq38
\[y'' - y' = \frac{b}{y}\]
Не решена
Найдено семейств: 0 / 1
Судья: Полнота не установлена
Ход решения: слабый
eq39
\[y'' = a\,x\,y^{-1/2}\]
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: средний
eq40
\[y\,y' = (3ax + b)\,y - a^2 x^3 - ab\,x^2 + cx\]
уравнение Абеля 2-го рода
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: сильный
eq41
\[y^{(4)} - c\,y'' = a\,e^{\lambda y} + b\,e^{2\lambda y}\]
искались частные решения
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: средний
Уравнения в частных производных
eq42
\[u_t = (u\,u_x)_x\]
уравнение Буссинеска; тестовая задача 1
Решена частично
Найдено семейств: 1 / 13
Судья: Решения подтверждены
Ход решения: слабый
eq43
\[u_{xx} = u_y\,u_{yy}\]
уравнение Гудерлея; тестовая задача 2
Решена частично
Найдено семейств: 2 / 6
Судья: Решения подтверждены
Ход решения: средний
eq44
\[u_t = u_{xx} + u_x^2 + k\,u^2\]
Решена частично
Найдено семейств: 1 / 4
Судья: Решения подтверждены
Ход решения: средний
eq45
\[u_y\,u_{xy} - u_x\,u_{yy} = u_{yyy}\]
пограничный слой; тестовая задача 4
Решена частично
Найдено семейств: 2 / 11
Судья: Решения подтверждены
Ход решения: сильный
eq46
\[u_t = (a\,x^n u_x)_x + b\,u \ln u\]
логарифмическая диффузия; тестовая задача 5
Решена частично
Найдено семейств: 1 / 4
Судья: Решения подтверждены
Ход решения: средний
eq47
\[u_t = u_{xx} + x^2 f(u)\]
тестовая задача 6
Решена частично
Найдено семейств: 1 / 3
Судья: Решения подтверждены
Ход решения: средний
eq48
\[u_t = (e^u u_x)_x\]
тестовая задача 7
Решена частично
Найдено семейств: 2 / 5
Судья: Решения подтверждены
Ход решения: слабый
eq49
\[i\,u_t + u_{xx} + f(|u|)\,u = 0\]
нелинейное уравнение Шрёдингера; тестовая задача 8
Решена частично
Найдено семейств: 1 / 10
Судья: Решения подтверждены
Ход решения: средний
eq50
\[u_t = u_{xx} + x^2 \cos u\]
тестовая задача 9
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: сильный
eq51
\[u_{xy}^2 - u_{xx}\,u_{yy} = f(x)\,y^k\]
уравнение типа Монжа–Ампера; тестовая задача 10
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: средний
eq52
\[u_{xy}^2 - u_{xx}\,u_{yy} = f(x)\,u^k\]
уравнение типа Монжа–Ампера
Не решена
Найдено семейств: 0 / 2
Судья: Полнота не установлена
Ход решения: слабый
eq53
\[u_t = u_{xx} + F(u, u_x)\]
обратная задача; тестовая задача 12
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: сильный
eq54
\[u_{xx}\,u_{yy} - u_{xy}^2 = f(x, y)\]
уравнение типа Монжа–Ампера; тестовая задача 13
Решена частично
Найдено семейств: 1 / 5
Судья: Решения подтверждены
Ход решения: слабый
eq55
\[u_{xxxx} + a\,u_{xxyy} + b\,u_{yyyy} = 0\]
анизотропная упругость; тестовая задача 14
Не решена
Найдено семейств: 0 / 7
Судья: Полнота не установлена
Ход решения: сильный
eq56
\[u_t = a\,u_{xx} + u\,f\bigl(u_x^2 - a u^2\bigr)\]
тестовая задача 15
Решена частично
Найдено семейств: 1 / 2
Судья: Решения подтверждены
Ход решения: слабый
eq57
\[u_{tt} = (x^k u_x)_x + f(u)\]
анизотропное уравнение Клейна–Гордона; тестовая задача 16
Решена частично
Найдено семейств: 1 / 4
Судья: Решения подтверждены
Ход решения: средний
eq58
\[u_{tt} = \bigl[f(u)\,u_x\bigr]_x\]
нелинейное волновое уравнение; тестовая задача 17
Решена частично
Найдено семейств: 1 / 3
Судья: Решения подтверждены
Ход решения: провал
eq59
\[u_t = \bigl[f(u)\,u_x\bigr]_x + \frac{a}{f(u)} + b\]
тестовая задача 18
Решена частично
Найдено семейств: 2 / 3
Судья: Решения подтверждены
Ход решения: сильный