Example solution 1: constant concentration source, n(x,t) = n₀ erfc(x / (2√(Dt)))

Proved

FickDiffusion.erfc_solution_constant_source

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

diffusionpde

Let $D>0$ and $n_0\in\mathbb R$ , and set

n(x,t)=n_0\,\operatorname{erfc}\Big(\frac{x}{2\sqrt{Dt}}\Big),\qquad \operatorname{erfc}(u)=\frac{2}{\sqrt\pi}\int_u^\infty e^{-s^2}ds .

Then:

$n$ satisfies Fick's second law: $\dfrac{\partial n}{\partial t}(x,t)=D\,\dfrac{\partial^2 n}{\partial x^2}(x,t)$ for all $x\in\mathbb R$ and $t>0$ ;
the boundary concentration is maintained: $n(0,t)=n_0$ for all $t>0$ ;
the medium is initially free of solute: for every $x>0$ , $n(x,t)\to0$ as $t\to0^+$ .

This is the classical solution for diffusion into a semi-infinite medium from a surface held at constant concentration $n_0$ .

Formalization Note Derivatives use Mathlib's deriv. Clause 2 is written with the literal argument $0/(2\sqrt{Dt})$ , i.e. $\operatorname{erfc}(0)$ .

Preamble

import Mathlib
import Definitions.Def_FickDiffusion_defs

open Real Filter Topology MeasureTheory

Formal statement

namespace FickDiffusion

theorem erfc_solution_constant_source (D n₀ : ℝ) (hD : 0 < D) :
    (∀ x t : ℝ, 0 < t →
      deriv (fun s => n₀ * erfc (x / (2 * Real.sqrt (D * s)))) t =
        D * deriv (fun y => deriv (fun z => n₀ * erfc (z / (2 * Real.sqrt (D * t)))) y) x) ∧
    (∀ t : ℝ, 0 < t → n₀ * erfc (0 / (2 * Real.sqrt (D * t))) = n₀) ∧
    (∀ x : ℝ, 0 < x →
      Tendsto (fun t => n₀ * erfc (x / (2 * Real.sqrt (D * t)))) (𝓝[>] 0) (𝓝 0)) := 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 "Example solution 1: constant concentration source and diffusion length" (p. 6), first displayed equation and the surrounding paragraph

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,n_0$ with $D>0$ , writing $\operatorname{erfc}(u)=\frac{2}{\sqrt\pi}\int_{(u,\infty)}e^{-s^2}ds$ and $N_t(z)=n_0\cdot\operatorname{erfc}\big(z/(2\sqrt{D t})\big)$ (real square root, $0$ on negatives; division by $0$ gives $0$ ), the following three statements all hold:

for all real $x$ and all $t>0$ : the derivative at $s=t$ of $s\mapsto n_0\operatorname{erfc}\big(x/(2\sqrt{Ds})\big)$ (a function on all of $\mathbb R$ ) equals $D$ times the derivative at $y=x$ of $y\mapsto\big(\text{derivative at } y \text{ of } N_t\big)$ ; derivatives are one-variable derivatives with value $0$ at non-differentiable points;
for all $t>0$ : $n_0\cdot\operatorname{erfc}\big(0/(2\sqrt{Dt})\big)=n_0$ ;
for every $x>0$ : $n_0\operatorname{erfc}\big(x/(2\sqrt{Dt})\big)\to0$ as $t\to0$ through values $t>0$ .

No condition is placed on the sign of $n_0$ ( $n_0=0$ and $n_0<0$ are allowed).

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