Cleo Bench

A mathematical benchmark built from 39 famously difficult questions answered by Cleo on Math Stack Exchange. It asks whether a model can derive the closed form.

39problems in the benchmark
22 / 23attempts with verified proofs
1proof additionally formalized in Lean

How the benchmark was made

We scraped Math Stack Exchange for Cleo’s questions and answers, then ran a three-stage process. This took about five Claude Max sessions.

  1. Numerical verification. We checked Cleo’s answers against high-precision numerical evaluations of the original questions, establishing the benchmark’s ground-truth answers.
  2. Derivation. Fable ran at maximum effort, with numerical tools and hours of working time, to derive solutions from each problem.
  3. Checking. Opus checked each proposed solution numerically and logically.

One proof has been formalized in Lean. Further autoformalization in Lean remains future work.

Context: the Cleo story

Levels of verification

Fable first works closed-book from the question alone. Its proposed closed form is numerically checked against Cleo’s answer and the original problem; an independent Opus grader then audits the derivation and recomputes the values at high precision. A verified proof has both the right value and a complete or mostly complete derivation.

proof verified correct value and audited derivationproof incomplete useful attempt, not counted as solvednot attempted benchmark item awaiting a run

Results

Each question title links to its original Math Stack Exchange post. “Read PDF” opens the typeset derivation; “TeX” downloads its source. The Lean link is the archived, buildable formalization for item 7.

MSE IDQuestionVerificationArtifacts
562694Integral $\int_{-1}^1\frac1x\sqrt{\frac{1+x}{1-x}}\ln\left(\frac{2\,x^2+2\,x+1}{2\,x^2-2\,x+1}\right) \mathrm dx$proof verifiedRead PDF TeX
712798Crazy $\int_0^\infty{_3F_2}\left(\begin{array}c\tfrac58,\tfrac58,\tfrac98\\\tfrac12,\tfrac{13}8\end{array}\middle|\ {-x}\right)^2\frac{dx}{\sqrt x}$proof verifiedRead PDF TeX
908108How to find ${\large\int}_0^1\frac{\ln^3(1+x)\ln x}x\mathrm dx$proof verifiedRead PDF TeX
1142705Evaluate $\int_0^{\pi/2}\frac{x^2\log^2{(\sin{x})}}{\sin^2x}dx$proof verifiedRead PDF TeX
1595389Integral ${\large\int}_0^{\pi/2}\arctan^2\!\left(\frac{\sin x}{\sqrt3+\cos x}\right)dx$proof equivalentRead PDF TeX
1588996Yet another log-sin integral $\int\limits_0^{\pi/3}\log(1+\sin x)\log(1-\sin x)\,dx$proof verifiedRead PDF TeX
418134Calculating $\int_{\pi/2}^{\pi}\frac{x\sin{x}}{5-4\cos{x}}\,\mathrm dx$proof verifiedRead PDF TeX Lean
1279165Integrals of the form ${\large\int}_0^\infty\operatorname{arccot}(x)\cdot\operatorname{arccot}(a\,x)\cdot\operatorname{arccot}(b\,x)\ dx$proof equivalentRead PDF TeX
905653How to find ${\large\int}_1^\infty\frac{1-x+\ln x}{x \left(1+x^2\right) \ln^2 x} \mathrm dx$?proof verifiedRead PDF TeX
714628Closed form for $\int_{-\infty}^0\operatorname{Ei}^3x\,dx$proof verifiedRead PDF TeX
918680Closed Form for the Imaginary Part of $\text{Li}_3\Big(\frac{1+i}2\Big)$proof equivalentRead PDF TeX
918821Closed form for ${\large\int}_0^1\frac{\ln^2x}{\sqrt{1-x+x^2}}dx$proof equivalentRead PDF TeX
1150822Closed form for $\int_0^\infty\arctan\Bigl(\frac{2\pi}{x-\ln\,x+\ln(\frac\pi2)}\Bigr)\frac{dx}{x+1}$proof verifiedRead PDF TeX
1376159A difficult logarithmic integral ${\Large\int}_0^1\log(x)\,\log(2+x)\,\log(1+x)\,\log\left(1+x^{-1}\right)dx$proof incompleteRead PDF TeX
970125Evaluate $\int_0^1\frac{\ln(1-x)}{x}\text{Li}_3\left(\frac{1+x}{2}\right)dx$ , $\int_0^1\frac{\ln^2(1-x)}{x}\text{Li}_2\left(\frac{1+x}{2} \right)dx$proof verifiedRead PDF TeX
1372767Integral $\int_0^1\frac{\log(x)\log(1+x)}{\sqrt{1-x}}\,dx$proof equivalentRead PDF TeX
1153708Closer form for $\int_0^\infty\frac{(\arctan{x})^2\log^2({1+x^2})}{x^2}dx$proof verifiedRead PDF TeX
570997Integral $\int_0^1\frac{\ln\left(x+\sqrt2\right)}{\sqrt{2-x}\,\sqrt{1-x}\,\sqrt{\vphantom{1}x}}\mathrm dx$proof verifiedRead PDF TeX
909228Infinite Series $\sum_{n=1}^\infty\frac{H_n}{n^32^n}$proof verifiedRead PDF TeX
1550806Closed form solution to $\int_0^1\arctan^2(x)\,\sqrt{x}\,dx$proof equivalentRead PDF TeX
564816Integral $\int_0^{\pi/2}\arctan^2\left(\frac{6\sin x}{3+\cos 2x}\right)\mathrm dx$proof verifiedRead PDF TeX
577849Derivative of the Meijer G-function with respect to one of its parametersproof verifiedRead PDF TeX
557439Integral $\int_0^\infty\frac{\operatorname{arccot}\left(\sqrt{x}-2\,\sqrt{x+1}\right)}{x+1}\mathrm dx$proof verifiedRead PDF TeX
554624Integral $\int_0^\infty\frac{1}{x\,\sqrt{2}+\sqrt{2\,x^2+1}}\cdot\frac{\log x}{\sqrt{x^2+1}}\mathrm dx$not attempted
927427Does $\int_0^1\frac{\ln x}{1+x}\cos^{-1}x\,\mathrm dx$ have a closed from?not attempted
577704Integral $\int_0^\infty\frac{\ln\left(1+x+\sqrt{x^2+2\,x}\right)\,\ln\left(1+\sqrt{x^2+2\,x+2}\right)}{x^2+2x+1}dx$not attempted
578605Integral $\int_0^\infty\frac{\ln\left(\sqrt{x+1\vphantom{x^0}}-1\right)\,\ln\left(\sqrt{x^{-1}+1}+1\right)}{(x+1)^{3/2}}dx$not attempted
702681Integral $\int_0^1\frac{\log(1-x)}{\sqrt{x-x^3}}dx$not attempted
935366Simplification of an expression containing $\operatorname{Li}_3(x)$ termsnot attempted
967398Extract real and imaginary parts of $\operatorname{Li}_2\left(i\left(2\pm\sqrt3\right)\right)$not attempted
930011Closed-forms for several tough integralsnot attempted
964438Integral $\int_0^1\frac{x^{42}}{\sqrt{x^4-x^2+1}}\operatorname d \!x$not attempted
572859Closed form for $\int_0^\infty\frac{\sin x\,\cdot\,\operatorname{Ci}x-\cos x\,\cdot\,\operatorname{Si}x}{\sqrt{16\,x^2+1}}dx$not attempted
581215Integral $\int_0^\infty x^2\,e^{-x^2}\operatorname{erf}(x)\,\log(x)\,dx$not attempted
904320Improper integral containing $\sqrt{\cos x-\frac1{\sqrt 2}}$ in the denominatornot attempted
710175Integral $\int_0^1\frac{\ln x}{x-1}\ln\left(1+\frac1{\ln^2x}\right)dx$not attempted
576304A closed form for $\int_0^1{_2F_1}\left(-\frac{1}{4},\frac{5}{4};\,1;\,\frac{x}{2}\right)^2dx$not attempted
704917Integral $\int_0^\infty F(x)\,F\left(x\,\sqrt2\right)\frac{e^{-x^2}}{x^2} \, dx$ involving Dawson's functionnot attempted
566513Closed form for $\int_0^1\sqrt{\frac{2-x}{(1-x)\,x}}\,\log\left(\frac{(2-x)\,x}{1-x}\right)dx$not attempted