∴ 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 · at least one of the handbook's solution families found — 49 · completeness proven — 3 (of which confirmed in Lean — 1) · per the judge's conclusions
What the statuses and labels mean
- Fully solved
- All reference solution families were found, and the completeness conclusion is proven and matches the reference.
- All known solutions found
- All reference solution families were found; completeness is not settled.
- Partially solved
- Some of the reference solution families were found.
- Not solved
- None of the reference solution families was found.
- Families found: k / n
- How many of the handbook's n solution families the agent found — per the LLM judge's final conclusion (the judge counts different forms of one family as one). Reference texts are not published.
- Judge
- The LLM judge's completeness verdict: proven, incompleteness proven, solutions verified (no completeness conclusion) or completeness open. For most problems completeness is not established in the handbook itself either.
- Completeness: Lean ✓
- The judge accepted completeness as proven, and the formal part of the completeness argument is checked in Lean 4. If the Lean code of the completeness node compiles but the judge did not accept completeness, there is no label — the problem report says so.
- Solution process
- A qualitative rating of the whole run from the final review of the IMV-2026 experiment — not only the answer but how the agent got there: depth of search, correctness of derivations, Lean backing, no false “new” solutions. Scale: strong, fair, weak, failed.
- Lean: k / m
- How many formal fragments passed the Lean 4 check (on the problem page). Compiling does not mean that a theorem about the problem statement itself is proven.
Algebraic equations
eq01
\[(a - x^2)^3 = (b - x^3)^2\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: strong
eq02
\[(x^3 + a)^3 + a = x\]
mo873.pdf: example 7, equation (33)
Fully solved
Families found: 1 / 1
Judge: Completeness proven
Completeness: Lean ✓
Solution process: strong
eq03
\[(x^3 + x + b)^3 + x^3 + 2b = 0\]
mo873.pdf: example 9, form (38) with \(f(x) = x^3,\ a = 1\)
Fully solved
Families found: 1 / 1
Judge: Completeness proven
Solution process: strong
eq04
\[2z^6 - 3\alpha z^4 - 2\beta z^3 + 3\alpha^2 z^2 + \beta^2 - \alpha^3 = 0\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: strong
eq05
\[x^5 - (a^4 - 3a^2 b + b^2)\,x + ab\,(a^2 - 2b) = 0\]
Fully solved
Families found: 2 / 2
Judge: Completeness proven
Solution process: strong
Functional equations
eq06
\[y(x)\,y(x+1) + a\,\bigl[y(x+1) - y(x)\bigr] = 0\]
All known solutions found
Families found: 1 / 1
Judge: Completeness open
Solution process: strong
eq07
\[y(\sin x) - y(\cos x) = 0\]
All known solutions found
Families found: 2 / 2
Judge: Solutions verified
Solution process: fair
eq08
\[y(x)\,y(a - x) = b^2\]
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: strong
eq09
\[f(x+y) + f(x-y) = 2f(x) + 2f(y)\]
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: strong
eq10
\[f(x, y) = a^n f\bigl(x + (1-a)\,y,\ a y\bigr)\]
All known solutions found
Families found: 2 / 2
Judge: Solutions verified
Solution process: fair
eq11
\[f(x+y) = f(x) + f(y) - a\,f(x)\,f(y)\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: weak
eq12
\[\sqrt{\frac{f(x)^2 + f(y)^2}{2}} = f\Bigl(\sqrt{\frac{x^2 + y^2}{2}}\Bigr)\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: strong
eq13
\[f(x+y) = g(x) + f(y) - f(x)\,h(y)\]
All known solutions found
Families found: 2 / 2
Judge: Completeness open
Solution process: strong
eq14
\[\begin{aligned} &f(t) + g(x)\,Q(z) + h(x)\,R(z) = 0,\\ &z = \varphi(x) + \psi(t) \end{aligned}\]
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: weak
Integral equations
eq15
\[\int_0^x \frac{y(t)}{\sqrt{x - t}}\,dt = f(x)\]
Abel integral equation of the first kind
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: fair
eq16
\[\int_0^x \cosh\bigl[a(x - t)\bigr]\,y(t)\,dt = f(x)\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: strong
eq17
\[\int_0^x \bigl\{\cosh\bigl[a(x - t)\bigr] + b\bigr\}\,y(t)\,dt = f(x)\]
Partially solved
Families found: 1 / 2
Judge: Completeness open
Solution process: fair
eq18
\[\int_0^x y(t)\,y(x - t)\,dt = ax + b\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: strong
eq19
\[y(x) + a\int_0^x (x - t)\,y(t)\,dt = f(x)\]
Partially solved
Families found: 1 / 2
Judge: Completeness open
Solution process: strong
eq20
\[a\,y(x) + \int_0^x y(t)\,y(x - t)\,dt = bx\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: strong
eq21
\[\int_{-\infty}^{\infty} e^{-\lambda|x - t|}\,y(t)\,dt = f(x)\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: weak
eq22
\[\int_{-\infty}^{\infty} \sin\bigl(\lambda|x - t|\bigr)\,y(t)\,dt = f(x)\]
Not solved
Families found: 0 / 1
Judge: Completeness open
Solution process: weak
eq23
\[y(x) + \lambda\int_0^{\infty} e^{-|x - t|}\,y(t)\,dt = f(x)\]
Wiener–Hopf equation of the second kind
Not solved
Families found: 0 / 2
Judge: Completeness open
Solution process: weak
eq24
\[y(x) - \lambda\int_{-\infty}^{\infty} e^{-|x - t|}\,y(t)\,dt = 0\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: fair
eq25
\[y(x) - \lambda\int_0^{\infty} \sin(xt)\,y(t)\,dt = f(x)\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: strong
eq26
\[y(x) + \int_a^b g(t)\,y(x)\,y(t)\,dt = f(x)\]
Not solved
Families found: 0 / 1
Judge: Solutions verified
Solution process: fair
Ordinary differential equations
eq27
\[y'' + f(x)\,y' + a\bigl[f(x) - a\bigr]\,y = 0\]
All known solutions found
Families found: 2 / 2
Judge: Solutions verified
Solution process: strong
eq28
\[x\,y'' + \bigl[x f(x) + a\bigr]\,y' + (a - 1)\,f(x)\,y = 0\]
Not solved
Families found: 0 / 2
Judge: Solutions verified
Solution process: weak
eq29
\[\begin{aligned} &x\,y'' + \bigl[(ax + 1)\,f(x) + ax - 1\bigr]\,y'\\ &\qquad + a^2 x\,f(x)\,y = 0 \end{aligned}\]
Not solved
Families found: 0 / 2
Judge: Completeness open
Solution process: weak
eq30
\[x^4\,y'' + (ax^2 + bx + c)\,y = 0\]
Partially solved
Families found: 1 / 2
Judge: Completeness open
Solution process: strong
eq31
\[(ax^2 + bx + c)^2\,y'' + y = 0\]
Not solved
Families found: 0 / 1
Judge: Completeness open
Solution process: fair
eq32
\[y\,y' - y = ax + b\]
Abel equation of the second kind
Partially solved
Families found: 1 / 2
Judge: Completeness open
Solution process: fair
eq33
\[y\,y' - y = ax + b\,e^{-2x/a}\]
Abel equation of the second kind
Not solved
Families found: 0 / 1
Judge: Completeness open
Solution process: weak
eq34
\[y\,y'' - (y')^2 = a\,y^3 e^{\lambda x}\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: strong
eq35
\[y'' = a\,y' + e^{2ax} f(y)\]
nonlinear, autonomous with exponential amplification
All known solutions found
Families found: 2 / 2
Judge: Solutions verified
Solution process: fair
eq36
\[y'' = \bigl[e^{ax} f(y) + a\bigr]\,y'\]
All known solutions found
Families found: 2 / 2
Judge: Solutions verified
Solution process: fair
eq37
\[y'' - a\,(y')^2 = f(x)\,e^{ay}\]
All known solutions found
Families found: 1 / 1
Judge: Solutions verified
Solution process: strong
eq38
\[y'' - y' = \frac{b}{y}\]
Not solved
Families found: 0 / 1
Judge: Completeness open
Solution process: weak
eq39
\[y'' = a\,x\,y^{-1/2}\]
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: fair
eq40
\[y\,y' = (3ax + b)\,y - a^2 x^3 - ab\,x^2 + cx\]
Abel equation of the second kind
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: strong
eq41
\[y^{(4)} - c\,y'' = a\,e^{\lambda y} + b\,e^{2\lambda y}\]
particular solutions were sought
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: fair
Partial differential equations
eq42
\[u_t = (u\,u_x)_x\]
Boussinesq equation; test problem 1
Partially solved
Families found: 1 / 13
Judge: Solutions verified
Solution process: weak
eq43
\[u_{xx} = u_y\,u_{yy}\]
Guderley equation; test problem 2
Partially solved
Families found: 2 / 6
Judge: Solutions verified
Solution process: fair
eq44
\[u_t = u_{xx} + u_x^2 + k\,u^2\]
Partially solved
Families found: 1 / 4
Judge: Solutions verified
Solution process: fair
eq45
\[u_y\,u_{xy} - u_x\,u_{yy} = u_{yyy}\]
boundary layer; test problem 4
Partially solved
Families found: 2 / 11
Judge: Solutions verified
Solution process: strong
eq46
\[u_t = (a\,x^n u_x)_x + b\,u \ln u\]
logarithmic diffusion; test problem 5
Partially solved
Families found: 1 / 4
Judge: Solutions verified
Solution process: fair
eq47
\[u_t = u_{xx} + x^2 f(u)\]
test problem 6
Partially solved
Families found: 1 / 3
Judge: Solutions verified
Solution process: fair
eq48
\[u_t = (e^u u_x)_x\]
test problem 7
Partially solved
Families found: 2 / 5
Judge: Solutions verified
Solution process: weak
eq49
\[i\,u_t + u_{xx} + f(|u|)\,u = 0\]
nonlinear Schrödinger equation; test problem 8
Partially solved
Families found: 1 / 10
Judge: Solutions verified
Solution process: fair
eq50
\[u_t = u_{xx} + x^2 \cos u\]
test problem 9
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: strong
eq51
\[u_{xy}^2 - u_{xx}\,u_{yy} = f(x)\,y^k\]
Monge–Ampère type equation; test problem 10
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: fair
eq52
\[u_{xy}^2 - u_{xx}\,u_{yy} = f(x)\,u^k\]
Monge–Ampère type equation
Not solved
Families found: 0 / 2
Judge: Completeness open
Solution process: weak
eq53
\[u_t = u_{xx} + F(u, u_x)\]
inverse problem; test problem 12
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: strong
eq54
\[u_{xx}\,u_{yy} - u_{xy}^2 = f(x, y)\]
Monge–Ampère type equation; test problem 13
Partially solved
Families found: 1 / 5
Judge: Solutions verified
Solution process: weak
eq55
\[u_{xxxx} + a\,u_{xxyy} + b\,u_{yyyy} = 0\]
anisotropic elasticity; test problem 14
Not solved
Families found: 0 / 7
Judge: Completeness open
Solution process: strong
eq56
\[u_t = a\,u_{xx} + u\,f\bigl(u_x^2 - a u^2\bigr)\]
test problem 15
Partially solved
Families found: 1 / 2
Judge: Solutions verified
Solution process: weak
eq57
\[u_{tt} = (x^k u_x)_x + f(u)\]
anisotropic Klein–Gordon equation; test problem 16
Partially solved
Families found: 1 / 4
Judge: Solutions verified
Solution process: fair
eq58
\[u_{tt} = \bigl[f(u)\,u_x\bigr]_x\]
nonlinear wave equation; test problem 17
Partially solved
Families found: 1 / 3
Judge: Solutions verified
Solution process: failed
eq59
\[u_t = \bigl[f(u)\,u_x\bigr]_x + \frac{a}{f(u)} + b\]
test problem 18
Partially solved
Families found: 2 / 3
Judge: Solutions verified
Solution process: strong