`Compfiles/Imo2016P4.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

15 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2016, Problem 4

A set of positive integers is called fragrant if it contains at least two elements and each of its elements has a prime factor in common with at least one of the other elements. Let P(n) = n² + n + 1. What is the least possible value of positive integer b such that there exists a non-negative integer a for which the set

{ P(a + 1), P(a + 2), ..., P(a + b) }

is fragrant?

Imports (2)

Imported by 1 file

Compfiles.lean

abbrev Imo2016P4.Fragrant line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, PNat
Proof uses: And, LE.le, Nat, OfNat.ofNat, Set.ncard, Membership.mem, Exists, Ne, Not, Nat.Coprime
4 instances, coercions and auxiliary constants left out.
abbrev Imo2016P4.P line 37 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, HPow.hPow, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
lemma Imo2016P4.P_inj line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Nat, Imo2016P4.P
Proof uses: StrictMono.injective, strictMono_nat_of_lt_succ, Eq.mpr, LT.lt, HAdd.hAdd, OfNat.ofNat, HPow.hPow, HMul.hMul, id, Eq, congr, congrArg, Eq.trans, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 36 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P4.ncard_set line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PNat, Eq, Set.ncard, Set.ofPred, Exists, And, LE.le, Imo2016P4.P, HAdd.hAdd
Proof uses: Set, Set.image, Subtype, LT.lt, OfNat.ofNat, Subtype.mk, add_pos', HPow.hPow, pow_pos, Right.add_pos_of_nonneg_of_pos, zero_le, PNat.pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Set.Icc, Set.ext, id and 30 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P4.two_not_dvd_P line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Dvd.dvd, OfNat.ofNat, Imo2016P4.P
Proof uses: HMul.hMul, HAdd.hAdd, Even.two_dvd, Nat.even_mul_succ_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P4.nine_not_dvd_P line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Dvd.dvd, OfNat.ofNat, Imo2016P4.P
Proof uses: Or, Eq, HMul.hMul, HAdd.hAdd, Exists, False, Exists.intro, HDiv.hDiv, Eq.symm
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P4.dvd_of_dvd_two_mul line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Dvd.dvd, OfNat.ofNat, HMul.hMul
Proof uses: Nat.Coprime.dvd_of_dvd_mul_left, Nat.Coprime.symm, Iff.mpr, Nat.Coprime, Nat.Prime.coprime_iff_not_dvd, Nat.prime_two
8 instances, coercions and auxiliary constants left out.
lemma Imo2016P4.gcd_P_dvd_of_eq A common divisor of P (b + k) and P b divides c whenever P (b + k) - P b = 2 * c, since values of P are odd line 79 source
Source documentation
A common divisor of P (b + k) and P b divides c whenever P (b + k) - P b = 2 * c, since values of P are odd.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, Imo2016P4.P, HMul.hMul, OfNat.ofNat, Dvd.dvd, Nat.gcd
Proof uses: Not, Imo2016P4.two_not_dvd_P, Dvd.dvd.trans, Nat.gcd_dvd_right, Imo2016P4.dvd_of_dvd_two_mul, Iff.mp, Nat.dvd_add_right, Eq.mpr, id, congrArg, Nat.gcd_dvd_left
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_P_dvd_of_eq {b k c : ℕ} (h : P b + 2 * c = P (b + k)) :
    (P (b + k)).gcd (P b) ∣ c := by
…
```
Mentions: h, Imo2016P4.P
lemma Imo2016P4.coprime_P_succ Adjacent values of P are coprime: a common divisor divides (P (b+1) - P b) / 2 = b + 1, hence divides P b - b*(b+1) = 1 line 89 source
Source documentation
Adjacent values of P are coprime: a common divisor divides (P (b+1) - P b) / 2 = b + 1, hence divides P b - b*(b+1) = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Coprime, Imo2016P4.P, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, Eq, Nat.gcd, id, congrArg, propext, Nat.coprime_iff_gcd_eq_one, Dvd.dvd, Imo2016P4.gcd_P_dvd_of_eq, Mathlib.Tactic.Ring.of_eq, HMul.hMul, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos and 35 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma coprime_P_succ (b : ℕ) : Nat.Coprime (P (b + 1)) (P b) := by
…
```
Mentions: Imo2016P4.P
lemma Imo2016P4.gcd_P_add_two_dvd The gcd of values of P at distance two divides 7 line 97 source
Source documentation
The gcd of values of P at distance two divides 7.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, Nat.gcd, Imo2016P4.P, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Nat.gcd_dvd_right, HMul.hMul, Imo2016P4.gcd_P_dvd_of_eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow and 31 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_P_add_two_dvd (b : ℕ) : (P (b + 2)).gcd (P b) ∣ 7 := by
…
```
Mentions: Imo2016P4.P
lemma Imo2016P4.gcd_P_add_three_dvd The gcd of values of P at distance three divides 3 line 110 source
Source documentation
The gcd of values of P at distance three divides 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, Nat.gcd, Imo2016P4.P, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Nat.gcd_dvd_right, HMul.hMul, Imo2016P4.gcd_P_dvd_of_eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow and 59 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_P_add_three_dvd (b : ℕ) : (P (b + 3)).gcd (P b) ∣ 3 := by
…
```
Mentions: Imo2016P4.P
lemma Imo2016P4.seven_dvd_P_of_not_coprime If values of P at distance two have a common factor, that factor is 7 line 134 source
Source documentation
If values of P at distance two have a common factor, that factor is 7.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Nat.Coprime, Imo2016P4.P, HAdd.hAdd, OfNat.ofNat, And, Dvd.dvd
Proof uses: Eq, Nat.gcd, Or.resolve_left, Iff.mp, Or, Nat.dvd_prime, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Imo2016P4.gcd_P_add_two_dvd, Eq.mp, congrArg, propext, Nat.coprime_iff_gcd_eq_one and 4 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma seven_dvd_P_of_not_coprime {b : ℕ} (h : ¬Nat.Coprime (P (b + 2)) (P b)) :
    7 ∣ P (b + 2) ∧ 7 ∣ P b := by
…
```
Mentions: h, Imo2016P4.P
lemma Imo2016P4.three_dvd_P_of_not_coprime If values of P at distance three have a common factor, that factor is 3 line 142 source
Source documentation
If values of P at distance three have a common factor, that factor is 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Nat.Coprime, Imo2016P4.P, HAdd.hAdd, OfNat.ofNat, And, Dvd.dvd
Proof uses: Eq, Nat.gcd, Or.resolve_left, Iff.mp, Or, Nat.dvd_prime, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Imo2016P4.gcd_P_add_three_dvd, Eq.mp, congrArg, propext, Nat.coprime_iff_gcd_eq_one and 3 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma three_dvd_P_of_not_coprime {b : ℕ} (h : ¬Nat.Coprime (P (b + 3)) (P b)) :
    3 ∣ P (b + 3) ∧ 3 ∣ P b := by
…
```
Mentions: h, Imo2016P4.P
determine Imo2016P4.Solution line 154 source
standard axioms: propext what this means
Statement uses: PNat
Proof uses: OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
problem Imo2016P4.imo2016_p4 line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, PNat, Set.ofPred, Exists, Nat, Imo2016P4.Fragrant, And, LE.le, Eq, Imo2016P4.P, HAdd.hAdd, Imo2016P4.Solution
Proof uses: Eq.mpr, OfNat.ofNat, id, congrArg, Imo2016P4.Solution.eq_1, And.intro, Membership.mem, Set, lowerBounds, Exists.intro, Set.ncard, Ne, Not, Nat.Coprime, Imo2016P4.ncard_set, of_eq_true, eq_true_of_decide, Eq.refl, Bool, Bool.true and 76 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 197 steps
Open to load the checked before-and-after goal states.