Решение — библиотека решённых задач · SciLib

∴ Библиотека решений

Решение

Уравнения прикладной математики из бенчмарка PolyaninBench, которые агент IMV решал на открытой модели gpt-oss-20b. Для каждой задачи — постановка (текст и Lean 4), найденные семейства решений, граф хода решения с формальными проверками и вывод о полноте. Вердикты выставил LLM-судья эксперимента IMV-2026; оценки людей появятся позже.

59 задач · gpt-oss-20b · совпадение хотя бы с одним семейством эталона — 44

Что означают метки
Совпало с эталоном: k / n
Сколько из n семейств решений справочника агент воспроизвёл. Тексты эталонов не публикуются.
Судья
Вердикт LLM-судьи о полноте: доказана, доказана неполнота, решения подтверждены (без вывода о полноте) или полнота не установлена.
Ход
Оценка прогона экспертом по итогам разбора эксперимента: сильный, средний, слабый, провал.
Lean: k / m
Сколько формальных фрагментов прошли проверку Lean 4. Компиляция не означает, что доказана теорема именно об условии задачи.

Алгебраические уравнения

eq01 (a - x^2)^3 = (b - x^3)^2
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: сильный Lean: 13 / 20
eq02 (x^3 + a)^3 + a = x (mo873.pdf Пример 7, ур-ние (33))
Совпало с эталоном: 1 / 1 Судья: Полнота доказана Ход: сильный Lean: 12 / 22
eq03 (x^3 + x + b)^3 + x^3 + 2 b = 0 (mo873.pdf Пример 9; форма (38), f(x)=x^3, a=1)
Совпало с эталоном: 1 / 2 Судья: Полнота доказана Ход: сильный Lean: 11 / 14
eq04 2 z^6 - 3 α z^4 - 2 β z^3 + 3 α^2 z^2 + β^2 - α^3 = 0
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: сильный Lean: 23 / 28
eq05 x ^ 5 - (a ^ 4 - 3 * a ^ 2 * b + b ^ 2) * x + a * b * (a ^ 2 - 2 * b) = 0
Совпало с эталоном: 2 / 2 Судья: Полнота доказана Ход: сильный Lean: 6 / 15

Функциональные уравнения

eq06 y(x) y(x+1) + a[y(x+1) - y(x)] = 0
Совпало с эталоном: 1 / 1 Судья: Полнота не установлена Ход: сильный Lean: 12 / 20
eq07 y(sin x) - y(cos x) = 0
Совпало с эталоном: 1 / 2 Судья: Решения подтверждены Ход: средний Lean: 10 / 15
eq08 y(x) y(a - x) = b^2
Совпало с эталоном: 1 / 2 Судья: Решения подтверждены Ход: сильный Lean: 11 / 17
eq09 f(x+y) + f(x-y) = 2 f(x) + 2 f(y)
Совпало с эталоном: 1 / 2 Судья: Решения подтверждены Ход: сильный Lean: 8 / 12
eq10 f(x,y) = a^n f(x + (1-a) y, a y)
Совпало с эталоном: 2 / 2 Судья: Решения подтверждены Ход: средний Lean: 15 / 28
eq11 f(x+y) = f(x) + f(y) - a f(x) f(y)
Совпало с эталоном: 0 / 1 Судья: Решения подтверждены Ход: слабый Lean: 14 / 24
eq12 sqrt((f(x)^2+f(y)^2)/2) = f(sqrt((x^2+y^2)/2))
Совпало с эталоном: 1 / 3 Судья: Решения подтверждены Ход: сильный Lean: 13 / 24
eq13 f(x+y) = g(x) + f(y) - f(x) h(y)
Совпало с эталоном: 2 / 2 Судья: Полнота не установлена Ход: сильный Lean: 18 / 36
eq14 f(t) + g(x) Q(z) + h(x) R(z) = 0, z = φ(x) + ψ(t)
Совпало с эталоном: 1 / 2 Судья: Решения подтверждены Ход: слабый Lean: 20 / 30

Интегральные уравнения

eq15 ∀ x, (∫ t in (0:ℝ)..x, y t / Real.sqrt (x - t)) = f x
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: средний Lean: 13 / 27
eq16 ∫_0^x cosh[a(x-t)] y(t) dt = f(x)
Совпало с эталоном: 1 / 3 Судья: Решения подтверждены Ход: сильный Lean: 9 / 12
eq17 ∫_0^x {cosh[a(x-t)] + b} y(t) dt = f(x)
Совпало с эталоном: 2 / 3 Судья: Полнота не установлена Ход: средний Lean: 2 / 17
eq18 ∫_0^x y(t) y(x-t) dt = a x + b
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: сильный Lean: 6 / 10
eq19 y(x) + a ∫_0^x (x-t) y(t) dt = f(x)
Совпало с эталоном: 1 / 2 Судья: Полнота не установлена Ход: сильный Lean: 14 / 23
eq20 a y(x) + ∫_0^x y(t) y(x-t) dt = b x
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: сильный Lean: 9 / 17
eq21 ∀ x, (∫ t, Real.exp (-lam * |x - t|) * y t) = f x
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: слабый Lean: 7 / 8
eq22 ∀ x, (∫ t, Real.sin (lam * |x - t|) * y t) = f x
Совпало с эталоном: 0 / 1 Судья: Полнота не установлена Ход: слабый Lean: 8 / 18
eq23 ∀ x, y x + lam * (∫ t in Set.Ioi (0:ℝ), Real.exp (-|x - t|) * y t) = f x
Совпало с эталоном: 0 / 2 Судья: Полнота не установлена Ход: слабый Lean: 11 / 22
eq24 ∀ x, y x - lam * (∫ t, Real.exp (-|x - t|) * y t) = 0
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: средний Lean: 7 / 17
eq25 ∀ x, y x - lam * (∫ t in Set.Ioi (0:ℝ), Real.sin (x * t) * y t) = f x
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: сильный Lean: 9 / 19
eq26 y(x) + ∫_a^b g(t) y(x) y(t) dt = f(x)
Совпало с эталоном: 0 / 2 Судья: Решения подтверждены Ход: средний Lean: 13 / 20

Обыкновенные дифференциальные уравнения

eq27 y'' + f(x) y' + a[f(x) - a] y = 0
Совпало с эталоном: 2 / 2 Судья: Решения подтверждены Ход: сильный Lean: 4 / 5
eq28 x y'' + [x f(x) + a] y' + (a-1) f(x) y = 0
Совпало с эталоном: 0 / 2 Судья: Решения подтверждены Ход: слабый Lean: 7 / 12
eq29 x y'' + [(ax+1) f(x) + ax - 1] y' + a² x f(x) y = 0
Совпало с эталоном: 0 / 2 Судья: Полнота не установлена Ход: слабый Lean: 4 / 20
eq30 ∀ x, x ^ 4 * deriv (deriv y) x + (a * x ^ 2 + b * x + c) * y x = 0
Совпало с эталоном: 1 / 2 Судья: Полнота не установлена Ход: сильный Lean: 15 / 28
eq31 ∀ x, (a * x ^ 2 + b * x + c) ^ 2 * deriv (deriv y) x + y x = 0
Совпало с эталоном: 0 / 1 Судья: Полнота не установлена Ход: средний Lean: 6 / 16
eq32 y y' - y = a x + b
Совпало с эталоном: 1 / 2 Судья: Полнота не установлена Ход: средний Lean: 14 / 26
eq33 ∀ x, y x * deriv y x - y x = a * x + b * Real.exp (-2 * x / a)
Совпало с эталоном: 0 / 1 Судья: Полнота не установлена Ход: слабый Lean: 9 / 18
eq34 ∀ x, y x * deriv (deriv y) x - (deriv y x) ^ 2 = a * y x ^ 3 * Real.exp (lam * x)
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: сильный Lean: 12 / 22
eq35 y'' = a y' + e^{2ax} f(y) (нелинейное автономно-усиленное)
Совпало с эталоном: 2 / 2 Судья: Решения подтверждены Ход: средний Lean: 9 / 20
eq36 y'' = [e^{a x} f(y) + a] y'
Совпало с эталоном: 2 / 2 Судья: Решения подтверждены Ход: средний Lean: 14 / 26
eq37 y'' - a (y')² = f(x) e^{a y}
Совпало с эталоном: 1 / 1 Судья: Решения подтверждены Ход: сильный Lean: 8 / 23
eq38 ∀ x, deriv (deriv y) x - deriv y x = b / y x
Совпало с эталоном: 0 / 1 Судья: Полнота не установлена Ход: слабый Lean: 9 / 18
eq39 y'' = a x y^{-1/2}
Совпало с эталоном: 1 / 2 Судья: Решения подтверждены Ход: средний Lean: 6 / 16
eq40 y y' = (3a x + b) y - a² x³ - a b x² + c x
Совпало с эталоном: 1 / 2 Судья: Решения подтверждены Ход: сильный Lean: 6 / 23
eq41 y'''' - c y'' = a e^{λy} + b e^{2λy} (искались частные решения)
Совпало с эталоном: 1 / 2 Судья: Решения подтверждены Ход: средний Lean: 11 / 26

Уравнения в частных производных

eq42 u_t = (u u_x)_x (уравнение Буссинеска; Тестовая задача 1)
Совпало с эталоном: 1 / 13 Судья: Решения подтверждены Ход: слабый Lean: 14 / 33
eq43 u_xx = u_y u_yy (уравнение Гудерлея; Тестовая задача 2)
Совпало с эталоном: 1 / 6 Судья: Решения подтверждены Ход: средний Lean: 10 / 26
eq44 ∀ t x, D1 u t x = D2 (D2 u) t x + (D2 u t x) ^ 2 + k * (u t x) ^ 2
Совпало с эталоном: 1 / 4 Судья: Решения подтверждены Ход: средний Lean: 26 / 38
eq45 u_y u_xy - u_x u_yy = u_yyy (погранслой; Тестовая задача 4)
Совпало с эталоном: 2 / 11 Судья: Решения подтверждены Ход: сильный Lean: 12 / 23
eq46 u_t = (a x^n u_x)_x + b u ln u (логарифм. диффузия; Тестовая задача 5)
Совпало с эталоном: 1 / 4 Судья: Решения подтверждены Ход: средний Lean: 13 / 26
eq47 u_t = u_xx + x² f(u) (Тестовая задача 6)
Совпало с эталоном: 1 / 3 Судья: Решения подтверждены Ход: средний Lean: 15 / 33
eq48 u_t = (e^u u_x)_x (Тестовая задача 7)
Совпало с эталоном: 0 / 5 Судья: Решения подтверждены Ход: слабый Lean: 9 / 22
eq49 i u_t + u_xx + f(|u|) u = 0 (нелинейное уравнение Шрёдингера; Тестовая задача 8)
Совпало с эталоном: 1 / 10 Судья: Решения подтверждены Ход: средний Lean: 18 / 28
eq50 u_t = u_xx + x² cos u (Тестовая задача 9)
Совпало с эталоном: 2 / 4 Судья: Решения подтверждены Ход: сильный Lean: 12 / 19
eq51 u_xy² − u_xx u_yy = f(x) y^k (Монж–Ампер; Тестовая задача 10)
Совпало с эталоном: 1 / 2 Судья: Решения подтверждены Ход: средний Lean: 14 / 31
eq52 ∀ x y, (D1 (D2 u) x y) ^ 2 - D1 (D1 u) x y * D2 (D2 u) x y = f x * (u x y) ^ k
Совпало с эталоном: 0 / 2 Судья: Полнота не установлена Ход: слабый Lean: 14 / 31
eq53 u_t = u_xx + F(u, u_x) (обратная задача; Тестовая задача 12)
Совпало с эталоном: 1 / 2 Судья: Решения подтверждены Ход: сильный Lean: 10 / 32
eq54 u_xx u_yy - u_xy^2 = f(x,y) (Монж–Ампер; Тестовая задача 13)
Совпало с эталоном: 0 / 5 Судья: Решения подтверждены Ход: слабый Lean: 13 / 28
eq55 u_xxxx + a u_xxyy + b u_yyyy = 0 (анизотропная упругость; Тестовая задача 14)
Совпало с эталоном: 0 / 7 Судья: Полнота не установлена Ход: сильный Lean: 12 / 32
eq56 u_t = a u_xx + u f(u_x² − a u²) (Тестовая задача 15)
Совпало с эталоном: 0 / 2 Судья: Решения подтверждены Ход: слабый Lean: 8 / 23
eq57 u_tt = (x^k u_x)_x + f(u) (анизотр. Клейн–Гордон; Тестовая задача 16)
Совпало с эталоном: 1 / 4 Судья: Решения подтверждены Ход: средний Lean: 20 / 31
eq58 u_tt = [f(u) u_x]_x (нелинейное волновое; Тестовая задача 17)
Совпало с эталоном: 0 / 3 Судья: Решения подтверждены Ход: провал Lean: 1 / 25
eq59 u_t = [f(u) u_x]_x + a/f(u) + b (Тестовая задача 18)
Совпало с эталоном: 2 / 3 Судья: Решения подтверждены Ход: сильный Lean: 3 / 18