Gaussian_Integral

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

definite-integrals-involving-exponential-functionproofwiki

$\displaystyle \int_{-\infty}^\infty e^{-x^2} \rd x = \sqrt \pi$

Preamble

import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Formal statement

theorem Gaussian_Integral : ∫ x : ℝ, Real.exp (-(x ^ 2)) = Real.sqrt Real.pi := by sorry

Source