$1/(x^2+1)$ has no antiderivative in $\mathbb{C}(x)$

Proved

LiouvilleDiffAlg.inv_X_sq_add_one_no_antideriv

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-algebrarational-functions

Equip $\mathbb{C}(x)$ with the standard derivative $D = d/dx$ . Then there is no rational function $g \in \mathbb{C}(x)$ with

Dg = \frac{1}{x^2+1}.

Its antiderivatives $\tan^{-1}(x) + C$ are therefore not rational. The next milestone shows that they nevertheless have the form required by Liouville's theorem.

Preamble

import Mathlib
import Definitions.Def_LiouvilleDiffAlg_RatFunc

open scoped Differential

Formal statement

namespace LiouvilleDiffAlg

theorem inv_X_sq_add_one_no_antideriv [Differential (RatFunc ℂ)] (hD : IsStandardDerivation) :
    ¬ ∃ g : RatFunc ℂ, g′ = 1 / (RatFunc.X ^ 2 + 1) := by sorry

end LiouvilleDiffAlg

Source

Wikipedia, "Liouville's theorem (differential algebra)", revision oldid=1349223559, https://en.wikipedia.org/w/index.php?title=Liouville%27s_theorem_(differential_algebra)&oldid=1349223559, section "Examples": "Likewise, the function

\frac{1}{x^2+1}

does not have an antiderivative in

\mathbb{C}(x)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements below (Aristotle, by Harmonic), with full knowledge of the source article and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; please compare it against the Lean code yourself.

Let $\mathbb{C}(x)$ carry a derivation $D$ (over $\mathbb{Z}$ ) with $D(p) = p'$ for every polynomial $p$ . Then there is no $g \in \mathbb{C}(x)$ with $Dg = 1/(x^2+1)$ . Here $x^2+1$ is a nonzero rational function, so $1/(x^2+1)$ involves no division by zero.

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

1/(x2+1)1/(x^2+1)1/(x2+1) has no antiderivative in C(x)\mathbb{C}(x)C(x)

$1/(x^2+1)$ has no antiderivative in $\mathbb{C}(x)$