Radical and the abc conjecture (Brocard mission)

Definition

Brocard_Defs

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

number-theory

This file introduces two notions used by the conditional milestone of the Brocard mission.

The radical of a natural number $n$ is

\operatorname{rad}(n) = \prod_{p \mid n,\ p \text{ prime}} p,

the product of the distinct primes dividing $n$ . By convention $\operatorname{rad}(0) = \operatorname{rad}(1) = 1$ .

The abc conjecture is the statement that for every real $\varepsilon > 0$ there is a real constant $K > 0$ such that for all positive integers $a, b$ with $\gcd(a,b) = 1$ and $c = a + b$ ,

c < K \cdot \operatorname{rad}(abc)^{1+\varepsilon}.

The abc conjecture is recorded as a proposition, to be used as a hypothesis; it is not asserted.

Formalization Note The power $\operatorname{rad}(abc)^{1+\varepsilon}$ is a real power of a positive real number. Coprimality is required only of $a$ and $b$ ; together with $a + b = c$ this makes $a, b, c$ pairwise coprime.

Definition code

import Mathlib

namespace Brocard

/-- The radical of a natural number `n`: the product of the distinct primes dividing `n`.
(With Mathlib's conventions `Nat.primeFactors 0 = ∅` and `Nat.primeFactors 1 = ∅`,
so `radical 0 = radical 1 = 1`.) -/
def radical (n : ℕ) : ℕ := ∏ p ∈ n.primeFactors, p

/-- The abc conjecture (Masser–Oesterlé), in its standard form: for every `ε > 0` there is a
constant `K > 0` such that every triple of positive integers `a, b, c` with `a` and `b`
coprime and `a + b = c` satisfies `c < K · rad(abc)^(1 + ε)`. -/
def ABCConjecture : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ K : ℝ, 0 < K ∧
    ∀ a b c : ℕ, 0 < a → 0 < b → Nat.Coprime a b → a + b = c →
      (c : ℝ) < K * (radical (a * b * c) : ℝ) ^ (1 + ε)

end Brocard

Source

Masser–Oesterlé abc conjecture (standard form), e.g. https://en.wikipedia.org/wiki/Abc_conjecture ; used as the hypothesis of Overholt, Bull. London Math. Soc. 25 (1993), 104.

Read-back

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

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements of this proposal, with full knowledge of the intended meaning and of the source material. It is not independent testimony and should not be treated as a blind audit; an independent read-back is still recommended before launch.

This definition file introduces, inside the namespace Brocard, one function and one proposition; it asserts no theorem.

1. Radical. For a natural number $n$ , $\operatorname{radical}(n)$ is the natural number

\operatorname{radical}(n) = \prod_{p \in \operatorname{primeFactors}(n)} p,

where $\operatorname{primeFactors}(n)$ is the finite set of primes dividing $n$ . For $n = 0$ and $n = 1$ this set is empty, so $\operatorname{radical}(0) = \operatorname{radical}(1) = 1$ (the empty product). For example $\operatorname{radical}(12) = 6$ and $\operatorname{radical}(49) = 7$ .

2. ABCConjecture. This is the proposition: for every real number $\varepsilon > 0$ there exists a real number $K > 0$ such that for all natural numbers $a, b, c$ satisfying

$a > 0$ and $b > 0$ ,
$\gcd(a, b) = 1$ ,
$a + b = c$ ,

the strict inequality

c < K \cdot \operatorname{radical}(a \cdot b \cdot c)^{1+\varepsilon}

holds, where the power is the real power of the real number $\operatorname{radical}(abc) \ge 1$ with real exponent $1 + \varepsilon$ , and $c$ and the radical are viewed as real numbers.

Edge cases: $c$ is automatically positive (at least $2$ ); $a \cdot b \cdot c$ is never $0$ , so the convention $\operatorname{radical}(0) = 1$ never enters. No coprimality of $c$ with $a$ or $b$ is required explicitly. The constant $K$ may depend on $\varepsilon$ but not on $a, b, c$ . The proposition is only defined here, not claimed to be true.

Human review

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

View graph