∴ Solution library
Solutions
Applied-mathematics equations from the PolyaninBench benchmark, solved by the IMV agent on the open model gpt-oss-20b. For every problem: the statement (text and Lean 4), the solution families found, the solution graph with formal checks, and the completeness conclusion. Verdicts come from the LLM judge of the IMV-2026 experiment; human reviews will follow.
59 problems · gpt-oss-20b · match with at least one reference family — 44
What the badges mean
- Matches reference: k / n
- How many of the n handbook solution families the agent reproduced. Reference texts are not published.
- Judge
- The LLM judge's completeness verdict: proven, incompleteness proven, solutions verified (no completeness conclusion) or completeness open.
- Run
- Expert rating of the run from the experiment review: strong, fair, weak, failed.
- Lean: k / m
- How many formal fragments passed the Lean 4 check. Compiling does not mean that a theorem about the problem condition itself is proven.
Algebraic equations
eq01
(a - x^2)^3 = (b - x^3)^2
Matches reference: 1 / 1
Judge: Solutions verified
Run: strong
Lean: 13 / 20
eq02
(x^3 + a)^3 + a = x (mo873.pdf Пример 7, ур-ние (33))
Matches reference: 1 / 1
Judge: Completeness proven
Run: strong
Lean: 12 / 22
eq03
(x^3 + x + b)^3 + x^3 + 2 b = 0 (mo873.pdf Пример 9; форма (38), f(x)=x^3, a=1)
Matches reference: 1 / 2
Judge: Completeness proven
Run: strong
Lean: 11 / 14
eq04
2 z^6 - 3 α z^4 - 2 β z^3 + 3 α^2 z^2 + β^2 - α^3 = 0
Matches reference: 1 / 1
Judge: Solutions verified
Run: strong
Lean: 23 / 28
eq05
x ^ 5 - (a ^ 4 - 3 * a ^ 2 * b + b ^ 2) * x + a * b * (a ^ 2 - 2 * b) = 0
Matches reference: 2 / 2
Judge: Completeness proven
Run: strong
Lean: 6 / 15
Functional equations
eq06
y(x) y(x+1) + a[y(x+1) - y(x)] = 0
Matches reference: 1 / 1
Judge: Completeness open
Run: strong
Lean: 12 / 20
eq07
y(sin x) - y(cos x) = 0
Matches reference: 1 / 2
Judge: Solutions verified
Run: fair
Lean: 10 / 15
eq08
y(x) y(a - x) = b^2
Matches reference: 1 / 2
Judge: Solutions verified
Run: strong
Lean: 11 / 17
eq09
f(x+y) + f(x-y) = 2 f(x) + 2 f(y)
Matches reference: 1 / 2
Judge: Solutions verified
Run: strong
Lean: 8 / 12
eq10
f(x,y) = a^n f(x + (1-a) y, a y)
Matches reference: 2 / 2
Judge: Solutions verified
Run: fair
Lean: 15 / 28
eq11
f(x+y) = f(x) + f(y) - a f(x) f(y)
Matches reference: 0 / 1
Judge: Solutions verified
Run: weak
Lean: 14 / 24
eq12
sqrt((f(x)^2+f(y)^2)/2) = f(sqrt((x^2+y^2)/2))
Matches reference: 1 / 3
Judge: Solutions verified
Run: strong
Lean: 13 / 24
eq13
f(x+y) = g(x) + f(y) - f(x) h(y)
Matches reference: 2 / 2
Judge: Completeness open
Run: strong
Lean: 18 / 36
eq14
f(t) + g(x) Q(z) + h(x) R(z) = 0, z = φ(x) + ψ(t)
Matches reference: 1 / 2
Judge: Solutions verified
Run: weak
Lean: 20 / 30
Integral equations
eq15
∀ x, (∫ t in (0:ℝ)..x, y t / Real.sqrt (x - t)) = f x
Matches reference: 1 / 1
Judge: Solutions verified
Run: fair
Lean: 13 / 27
eq16
∫_0^x cosh[a(x-t)] y(t) dt = f(x)
Matches reference: 1 / 3
Judge: Solutions verified
Run: strong
Lean: 9 / 12
eq17
∫_0^x {cosh[a(x-t)] + b} y(t) dt = f(x)
Matches reference: 2 / 3
Judge: Completeness open
Run: fair
Lean: 2 / 17
eq18
∫_0^x y(t) y(x-t) dt = a x + b
Matches reference: 1 / 1
Judge: Solutions verified
Run: strong
Lean: 6 / 10
eq19
y(x) + a ∫_0^x (x-t) y(t) dt = f(x)
Matches reference: 1 / 2
Judge: Completeness open
Run: strong
Lean: 14 / 23
eq20
a y(x) + ∫_0^x y(t) y(x-t) dt = b x
Matches reference: 1 / 1
Judge: Solutions verified
Run: strong
Lean: 9 / 17
eq21
∀ x, (∫ t, Real.exp (-lam * |x - t|) * y t) = f x
Matches reference: 1 / 1
Judge: Solutions verified
Run: weak
Lean: 7 / 8
eq22
∀ x, (∫ t, Real.sin (lam * |x - t|) * y t) = f x
Matches reference: 0 / 1
Judge: Completeness open
Run: weak
Lean: 8 / 18
eq23
∀ x, y x + lam * (∫ t in Set.Ioi (0:ℝ), Real.exp (-|x - t|) * y t) = f x
Matches reference: 0 / 2
Judge: Completeness open
Run: weak
Lean: 11 / 22
eq24
∀ x, y x - lam * (∫ t, Real.exp (-|x - t|) * y t) = 0
Matches reference: 1 / 1
Judge: Solutions verified
Run: fair
Lean: 7 / 17
eq25
∀ x, y x - lam * (∫ t in Set.Ioi (0:ℝ), Real.sin (x * t) * y t) = f x
Matches reference: 1 / 1
Judge: Solutions verified
Run: strong
Lean: 9 / 19
eq26
y(x) + ∫_a^b g(t) y(x) y(t) dt = f(x)
Matches reference: 0 / 2
Judge: Solutions verified
Run: fair
Lean: 13 / 20
Ordinary differential equations
eq27
y'' + f(x) y' + a[f(x) - a] y = 0
Matches reference: 2 / 2
Judge: Solutions verified
Run: strong
Lean: 4 / 5
eq28
x y'' + [x f(x) + a] y' + (a-1) f(x) y = 0
Matches reference: 0 / 2
Judge: Solutions verified
Run: weak
Lean: 7 / 12
eq29
x y'' + [(ax+1) f(x) + ax - 1] y' + a² x f(x) y = 0
Matches reference: 0 / 2
Judge: Completeness open
Run: weak
Lean: 4 / 20
eq30
∀ x, x ^ 4 * deriv (deriv y) x + (a * x ^ 2 + b * x + c) * y x = 0
Matches reference: 1 / 2
Judge: Completeness open
Run: strong
Lean: 15 / 28
eq31
∀ x, (a * x ^ 2 + b * x + c) ^ 2 * deriv (deriv y) x + y x = 0
Matches reference: 0 / 1
Judge: Completeness open
Run: fair
Lean: 6 / 16
eq32
y y' - y = a x + b
Matches reference: 1 / 2
Judge: Completeness open
Run: fair
Lean: 14 / 26
eq33
∀ x, y x * deriv y x - y x = a * x + b * Real.exp (-2 * x / a)
Matches reference: 0 / 1
Judge: Completeness open
Run: weak
Lean: 9 / 18
eq34
∀ x, y x * deriv (deriv y) x - (deriv y x) ^ 2 = a * y x ^ 3 * Real.exp (lam * x)
Matches reference: 1 / 1
Judge: Solutions verified
Run: strong
Lean: 12 / 22
eq35
y'' = a y' + e^{2ax} f(y) (нелинейное автономно-усиленное)
Matches reference: 2 / 2
Judge: Solutions verified
Run: fair
Lean: 9 / 20
eq36
y'' = [e^{a x} f(y) + a] y'
Matches reference: 2 / 2
Judge: Solutions verified
Run: fair
Lean: 14 / 26
eq37
y'' - a (y')² = f(x) e^{a y}
Matches reference: 1 / 1
Judge: Solutions verified
Run: strong
Lean: 8 / 23
eq38
∀ x, deriv (deriv y) x - deriv y x = b / y x
Matches reference: 0 / 1
Judge: Completeness open
Run: weak
Lean: 9 / 18
eq39
y'' = a x y^{-1/2}
Matches reference: 1 / 2
Judge: Solutions verified
Run: fair
Lean: 6 / 16
eq40
y y' = (3a x + b) y - a² x³ - a b x² + c x
Matches reference: 1 / 2
Judge: Solutions verified
Run: strong
Lean: 6 / 23
eq41
y'''' - c y'' = a e^{λy} + b e^{2λy} (искались частные решения)
Matches reference: 1 / 2
Judge: Solutions verified
Run: fair
Lean: 11 / 26
Partial differential equations
eq42
u_t = (u u_x)_x (уравнение Буссинеска; Тестовая задача 1)
Matches reference: 1 / 13
Judge: Solutions verified
Run: weak
Lean: 14 / 33
eq43
u_xx = u_y u_yy (уравнение Гудерлея; Тестовая задача 2)
Matches reference: 1 / 6
Judge: Solutions verified
Run: fair
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
Matches reference: 1 / 4
Judge: Solutions verified
Run: fair
Lean: 26 / 38
eq45
u_y u_xy - u_x u_yy = u_yyy (погранслой; Тестовая задача 4)
Matches reference: 2 / 11
Judge: Solutions verified
Run: strong
Lean: 12 / 23
eq46
u_t = (a x^n u_x)_x + b u ln u (логарифм. диффузия; Тестовая задача 5)
Matches reference: 1 / 4
Judge: Solutions verified
Run: fair
Lean: 13 / 26
eq47
u_t = u_xx + x² f(u) (Тестовая задача 6)
Matches reference: 1 / 3
Judge: Solutions verified
Run: fair
Lean: 15 / 33
eq48
u_t = (e^u u_x)_x (Тестовая задача 7)
Matches reference: 0 / 5
Judge: Solutions verified
Run: weak
Lean: 9 / 22
eq49
i u_t + u_xx + f(|u|) u = 0 (нелинейное уравнение Шрёдингера; Тестовая задача 8)
Matches reference: 1 / 10
Judge: Solutions verified
Run: fair
Lean: 18 / 28
eq50
u_t = u_xx + x² cos u (Тестовая задача 9)
Matches reference: 2 / 4
Judge: Solutions verified
Run: strong
Lean: 12 / 19
eq51
u_xy² − u_xx u_yy = f(x) y^k (Монж–Ампер; Тестовая задача 10)
Matches reference: 1 / 2
Judge: Solutions verified
Run: fair
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
Matches reference: 0 / 2
Judge: Completeness open
Run: weak
Lean: 14 / 31
eq53
u_t = u_xx + F(u, u_x) (обратная задача; Тестовая задача 12)
Matches reference: 1 / 2
Judge: Solutions verified
Run: strong
Lean: 10 / 32
eq54
u_xx u_yy - u_xy^2 = f(x,y) (Монж–Ампер; Тестовая задача 13)
Matches reference: 0 / 5
Judge: Solutions verified
Run: weak
Lean: 13 / 28
eq55
u_xxxx + a u_xxyy + b u_yyyy = 0 (анизотропная упругость; Тестовая задача 14)
Matches reference: 0 / 7
Judge: Completeness open
Run: strong
Lean: 12 / 32
eq56
u_t = a u_xx + u f(u_x² − a u²) (Тестовая задача 15)
Matches reference: 0 / 2
Judge: Solutions verified
Run: weak
Lean: 8 / 23
eq57
u_tt = (x^k u_x)_x + f(u) (анизотр. Клейн–Гордон; Тестовая задача 16)
Matches reference: 1 / 4
Judge: Solutions verified
Run: fair
Lean: 20 / 31
eq58
u_tt = [f(u) u_x]_x (нелинейное волновое; Тестовая задача 17)
Matches reference: 0 / 3
Judge: Solutions verified
Run: failed
Lean: 1 / 25
eq59
u_t = [f(u) u_x]_x + a/f(u) + b (Тестовая задача 18)
Matches reference: 2 / 3
Judge: Solutions verified
Run: strong
Lean: 3 / 18