`Compfiles/Usa1982P1.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

12 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1982, Problem 1

A graph has 1982 points. Given any four points, there is at least one joined to the other three. What is the smallest number of points which are joined to 1981 points?

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa1982P1.FourPointProperty The hypothesis of the problem: among any four vertices of the graph, some vertex is adjacent to the other three line 33 source
Source documentation
The hypothesis of the problem: among any four vertices of the graph, some vertex is adjacent to the other three.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: Finset, Eq, Finset.card, Exists, And, Membership.mem, Ne, SimpleGraph.Adj
4 instances, coercions and auxiliary constants left out.
```
def FourPointProperty (G : SimpleGraph (Fin 1982)) : Prop :=
…
```
def Usa1982P1.IsUniversal A vertex is universal if it is joined to all 1981 other vertices line 37 source
Source documentation
A vertex is universal if it is joined to all 1981 other vertices.

no axioms what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: Ne, SimpleGraph.Adj
2 instances, coercions and auxiliary constants left out.
```
def IsUniversal (G : SimpleGraph (Fin 1982)) (v : Fin 1982) : Prop :=
…
```
determine Usa1982P1.solution line 40 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
lemma Usa1982P1.card_four_of_distinct A finset of four distinct vertices has cardinality four line 45 source
Source documentation
A finset of four distinct vertices has cardinality four.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Eq, Finset.card, Insert.insert, Finset, Singleton.singleton
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, Finset.card_insert_of_notMem, of_eq_true, Not, Membership.mem, Eq.trans, False, True, Or, congr, eq_false, or_self, not_false_eq_true, Finset.card_singleton, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma card_four_of_distinct {a b c d : Fin 1982} (hab : a ≠ b) (hac : a ≠ c)
    (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) :
    ({a, b, c, d} : Finset (Fin 1982)).card = 4 := by
…
```
lemma Usa1982P1.card_universal_ge Lower bound: in any graph satisfying FourPointProperty, at most three vertices fail to be universal, so at least 1979 vertices are universal line 64 source
Source documentation
Lower bound: in any graph satisfying FourPointProperty, at most three vertices fail to be universal, so at least 1979 vertices are universal.
The proof follows the official solution. Suppose four vertices were not universal. Let A be one of them and let B be a vertex not joined to A. Then any two other vertices X, Y must be joined (else no vertex of {A, B, X, Y} would be joined to the other three). Take two further non-universal vertices C, D ∉ {A, B}. Each of C, D is joined to every vertex except possibly A and B, and being non-universal it must miss one of those. But then no vertex of {A, B, C, D} is joined to the other three, a contradiction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat, Usa1982P1.FourPointProperty, LE.le, Finset.card, Finset.filter, Usa1982P1.IsUniversal, Classical.propDecidable, Finset.univ
Proof uses: Finset, Not, Eq, rfl, HAdd.hAdd, Finset.card_filter_add_card_filter_not, Eq.mp, Fintype.card, congrArg, Fintype.card_fin, Finset.card_univ, Decidable.byContradiction, Membership.mem, Finset.Nonempty, False, Iff.mp, LT.lt, Finset.card_pos, And.right, And and 35 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 105 steps
Open to load the checked before-and-after goal states.
```
lemma card_universal_ge (G : SimpleGraph (Fin 1982)) (hG : FourPointProperty G) :
    1979 ≤ (Finset.univ.filter (IsUniversal G)).card := by
…
```
Mentions: Usa1982P1.FourPointProperty, Usa1982P1.IsUniversal
lemma Usa1982P1.card_three The finset {0, 1, 2} of vertices has three elements line 153 source
Source documentation
The finset {0, 1, 2} of vertices has three elements.

standard axioms: Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Fin, OfNat.ofNat, Insert.insert, Finset, Singleton.singleton
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma card_three : ({0, 1, 2} : Finset (Fin 1982)).card = 3 := by decide
```
def Usa1982P1.extremalAdj Adjacency in the extremal graph: all pairs of distinct vertices except 0—1 and 0—2 line 157 source
Source documentation
Adjacency in the extremal graph: all pairs of distinct vertices except 0—1 and 0—2.

standard axioms: propext what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: And, Ne, Not, Or, Eq
4 instances, coercions and auxiliary constants left out.
```
def extremalAdj (i j : Fin 1982) : Prop :=
…
```
def Usa1982P1.extremalGraph The extremal graph: the complete graph on Fin 1982 with the two edges 0—1 and 0—2 removed line 162 source
Source documentation
The extremal graph: the complete graph on Fin 1982 with the two edges 0—1 and 0—2 removed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: SimpleGraph.mk, Usa1982P1.extremalAdj
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def extremalGraph : SimpleGraph (Fin 1982) where
…
```
lemma Usa1982P1.extremal_universal_iff In the extremal graph, the universal vertices are exactly those outside {0, 1, 2} line 169 source
Source documentation
In the extremal graph, the universal vertices are exactly those outside {0, 1, 2}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Iff, Usa1982P1.IsUniversal, Usa1982P1.extremalGraph, And, Ne
Proof uses: Iff.intro, Decidable.byContradiction, Eq, Not, Or, Iff.mp, Decidable.not_and_iff_not_or_not', Iff.mpr, Classical.or_iff_not_imp_left, False.elim, Decidable.of_not_not, False, Usa1982P1.extremalAdj, And.right, Or.inl, And.intro, rfl, of_decide_eq_true, id, Bool and 7 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma extremal_universal_iff (v : Fin 1982) :
    IsUniversal extremalGraph v ↔ v ≠ 0 ∧ v ≠ 1 ∧ v ≠ 2 := by
…
```
Mentions: Usa1982P1.IsUniversal, Usa1982P1.extremalGraph
lemma Usa1982P1.extremal_fourPoint The extremal graph satisfies the four-point condition: any four vertices contain one outside {0, 1, 2}, and that vertex is joined to all others line 195 source
Source documentation
The extremal graph satisfies the four-point condition: any four vertices contain one outside {0, 1, 2}, and that vertex is joined to all others.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1982P1.FourPointProperty, Usa1982P1.extremalGraph
Proof uses: Finset, Fin, OfNat.ofNat, Nat, Eq, Finset.card, And, Membership.mem, Not, Insert.insert, Singleton.singleton, Exists, Ne, SimpleGraph.Adj, Decidable.byContradiction, LE.le, Exists.intro, And.intro, Finset.card_le_card, absurd and 14 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma extremal_fourPoint : FourPointProperty extremalGraph := by
…
```
Mentions: Usa1982P1.FourPointProperty, Usa1982P1.extremalGraph
lemma Usa1982P1.extremal_count The extremal graph has exactly 1979 universal vertices line 211 source
Source documentation
The extremal graph has exactly 1979 universal vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Fin, OfNat.ofNat, Finset.filter, Usa1982P1.IsUniversal, Usa1982P1.extremalGraph, Classical.propDecidable, Finset.univ
Proof uses: Finset, SDiff.sdiff, Insert.insert, Singleton.singleton, Finset.ext, Eq.mpr, Iff, Membership.mem, Not, Or, id, congr, congrArg, Eq.trans, And, True, congrFun', true_and, Ne, propext and 16 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma extremal_count :
    (Finset.univ.filter (IsUniversal extremalGraph)).card = 1979 := by
…
```
Mentions: Usa1982P1.IsUniversal, Usa1982P1.extremalGraph
problem Usa1982P1.usa1982_p1 line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, SimpleGraph, Fin, OfNat.ofNat, And, Usa1982P1.FourPointProperty, Eq, Finset.card, Finset.filter, Usa1982P1.IsUniversal, Classical.propDecidable, Finset.univ, Usa1982P1.solution
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Exists.intro, Usa1982P1.extremalGraph, Usa1982P1.extremal_fourPoint, Eq.symm, Usa1982P1.extremal_count, LE.le, Eq.mpr, id, congrArg, Usa1982P1.card_universal_ge
9 instances, coercions and auxiliary constants left out.

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