Kontsevich and Zagier define a period as an integral of a rational function (over $\mathbb{Q}$) defined on a $\mathbb{Q}$-semialgebraic set. They conjecture that if two periods are equal, then the reason may be only a finite number of change of variables and integrations by parts. The question is whether there is a clever computer system which checks whether two periods are equal and if they are, provide a proof (which is the aforementioned sequence.)

A particular motivation is the following identity \begin{align*} 7\int_0^1\log x\cdot \frac{1+x-x^2+x^3-x^4-x^5}{1-x^7}dx=\\ 12\int_{\frac{\sqrt{21}-5}2}^1 \frac{\log|x|}{2+3x+2x^2}dx. \end{align*}

Both parts are periods as may be easily seen if we expand $$\log |x|=\int_{|x|}^1 y^{-1}dy = p.v.\int_{x}^1 y^{-1} dy$$ and so get integrals of rational functions over triangles (if we are ok with p.v.) or triangle/quadrilateral.

Richard Stanley reminds us in this answer at MathOverflow that this is still a conjecture. It comes from the volumes of hyperbolic tetrahedra and it may be proved that the ratio of two sides is a rational number(!), which is calculated and coincides with 1 with accuracy of about 20000 decimal digits.

It is a bit annoying if neither a general theory nor programs motivated by this theory can provide a way to verify such a seemingly toy identity.