The 1D diffusion kernel satisfies Fick's second law

Proved

FickDiffusion.heatKernel_fick_second_law

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

diffusionpde

Let $D>0$ and let

\varphi_D(x,t)=\frac{1}{\sqrt{4\pi Dt}}\exp\Big(-\frac{x^2}{4Dt}\Big).

Then for every $x\in\mathbb R$ and every $t>0$ ,

\frac{\partial\varphi_D}{\partial t}(x,t)=D\,\frac{\partial^2\varphi_D}{\partial x^2}(x,t).

This is the statement that the Gaussian kernel is a classical solution of Fick's second law (the one-dimensional diffusion equation) for positive times.

Formalization Note Both sides are written with Mathlib's one-variable deriv; the kernel is smooth on $\{t>0\}$ , so these are the genuine partial derivatives.

Preamble

import Mathlib
import Definitions.Def_FickDiffusion_defs

open Real Filter Topology MeasureTheory

Formal statement

namespace FickDiffusion

theorem heatKernel_fick_second_law (D : ℝ) (hD : 0 < D) (x t : ℝ) (ht : 0 < t) :
    deriv (fun s => heatKernel D x s) t =
      D * deriv (fun y => deriv (fun z => heatKernel D z t) y) x := by sorry

end FickDiffusion

Source

Wikipedia, "Fick's laws of diffusion" (PDF snapshot supplied by the proposer, 21 pp.), https://en.wikipedia.org/wiki/Fick%27s_laws_of_diffusion, section "Fick's second law" (p. 4), last displayed equation, and the one-dimensional equation at the top of the section

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter (non-blind)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements, with full knowledge of the source and of the intended meaning, at the explicit instruction of the account owner. It is not a blind audit. Reviewers must not treat it as independent evidence of faithfulness and should compare it directly against the Lean code.

For all real $D,x,t$ with $D>0$ and $t>0$ : write $K(y,s)=\dfrac{1}{\sqrt{4\pi D s}}\exp\!\big(-y^2/(4Ds)\big)$ (the function heatKernel D y s; $\sqrt{\cdot}$ is the real square root, $0$ on negatives, and division by $0$ gives $0$ ). The statement asserts

\frac{d}{ds}\Big|_{s=t}K(x,s)\;=\;D\cdot\frac{d}{dy}\Big|_{y=x}\Big(\frac{d}{dz}\Big|_{z=y}K(z,t)\Big),

where each $\frac{d}{d\cdot}$ is the one-variable derivative with the convention "value $0$ where not differentiable". The time derivative is taken of the full function $s\mapsto K(x,s)$ on all of $\mathbb R$ (including $s\le 0$ , where $K$ is $0$ ), but only evaluated at the point $s=t>0$ .

Human review

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

View graph