794.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 10 curated AI-written annotations and 7190 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 project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 794

References:

erdosproblems.com/794
[Er69] Erdős, Paul, Some applications of graph theory to number theory. The Many Facets of Graph Theory (Proc. Conf., Western Mich. Univ., Kalamazoo, Mich., 1968) (1969), 77-82.
[FrFu84] Frankl, P. and Füredi, Z., An exact result for $3$-graphs. Discrete Math. (1984), 323-328.

Imports (1)

FormalConjecturesUtil

def Erdos794.harrisHypergraph Documented declaration: harrisHypergraph line 41 source
Source documentation
The 3-uniform hypergraph on Fin 9 given by Harris: the 27 triples containing exactly one vertex from each of the three parts {0, 1, 2}, {3, 4, 5}, {6, 7, 8}, together with the triple {0, 1, 2}. A triple is a transversal of the three parts exactly when the three values of v ↦ v / 3 it produces are distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat
Proof uses: Insert.insert, Singleton.singleton, Finset.filter, Eq, Finset.card, Finset.image, HDiv.hDiv, Finset.powersetCard, Finset.univ
13 instances, coercions and auxiliary constants left out.
```
def harrisHypergraph : Finset (Finset (Fin 9)) :=
…
```
theorem Erdos794.erdos_794 Documented declaration: erdos_794 sorry line 58 source
Source documentation
Is it true that every $3$-uniform hypergraph on $3n$ vertices with at least $n^3+1$ edges must contain either a subgraph on $4$ vertices with $3$ edges or a subgraph on $5$ vertices with $7$ edges?
Harris has provided the following simple counterexample to the problem as stated: the $3$-uniform graph on $\{1,\ldots,9\}$ with $28$ edges, formed by taking $27$ edges by choosing one element each from $\{1,2,3\},\{4,5,6\},\{7,8,9\}$, and then adding the edge $\{1,2,3\}$.

depends on sorry what this means
Statement uses: Iff, False, Nat, Finset, Fin, HMul.hMul, OfNat.ofNat, Finset.IsUniform, LE.le, HAdd.hAdd, HPow.hPow, Finset.card, Or, Finset.ContainsSubgraph
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_794 : answer(False) ↔
    ∀ n : ℕ, ∀ H : Finset (Finset (Fin (3 * n))), H.IsUniform 3 →
      n ^ 3 + 1 ≤ H.card → H.ContainsSubgraph 4 3 ∨ H.ContainsSubgraph 5 7 := by
…
```
theorem Erdos794.erdos_794.variants.balogh Documented declaration: balogh line 69 source
Source documentation
Balogh has observed that this problem is probably misstated by Erdős - indeed, every graph with $5$ vertices spanning $7$ edges contains a graph on $4$ vertices spanning $3$ edges, so the second condition can be dropped.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Finset.IsUniform, OfNat.ofNat, Nat, Finset.ContainsSubgraph
Proof uses: And, Eq, Finset.card, LE.le, Finset.filter, Classical.byContradiction, Not, Finset.sum, Finset.powersetCard, Trans.trans, Finset.sum_le_sum, Membership.mem, LT.lt, Eq.mp, Eq.trans, Exists, forall_congr, implies_congr, Eq.refl, And.right and 37 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_794.variants.balogh {V : Type*} [DecidableEq V] (H : Finset (Finset V))
    (hH : H.IsUniform 3) (h : H.ContainsSubgraph 5 7) : H.ContainsSubgraph 4 3 := by
…
```
theorem Erdos794.erdos_794.variants.harris Documented declaration: harris line 108 source
Source documentation
Harris has provided the following simple counterexample to the problem as stated: the $3$-uniform graph on $\{1,\ldots,9\}$ with $28$ edges, formed by taking $27$ edges by choosing one element each from $\{1,2,3\},\{4,5,6\},\{7,8,9\}$, and then adding the edge $\{1,2,3\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Finset.IsUniform, Fin, OfNat.ofNat, Nat, Erdos794.harrisHypergraph, Eq, Finset.card, Finset, Not, Finset.ContainsSubgraph
Proof uses: id, Membership.mem
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_794.variants.harris :
    harrisHypergraph.IsUniform 3 ∧ harrisHypergraph.card = 28 ∧
      ¬ harrisHypergraph.ContainsSubgraph 4 3 ∧ ¬ harrisHypergraph.ContainsSubgraph 5 7 := by
…
```
theorem Erdos794.erdos_794.variants.frankl_furedi This problem is then now asking how many edges a $3$-uniform hypergraph can have before it contains $K_4$ minus an edge, and whether the critical edge density is $2/9$ sorry line 122 source
Source documentation
This problem is then now asking how many edges a $3$-uniform hypergraph can have before it contains $K_4$ minus an edge, and whether the critical edge density is $2/9$. In fact there is a construction of Frankl and Füredi [FrFu84] showing it must be at least $2/7$, which is the conjectured truth (although Turán conjectured before [Er69] that the edge density was $1/4$, and so likely there is simply a typo in this problem's statement).

depends on sorry what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Exists, Finset, Fin, And, Finset.IsUniform, Not, Finset.ContainsSubgraph, LE.le, HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.choose, Finset.card, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_794.variants.frankl_furedi (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n : ℕ in atTop, ∃ H : Finset (Finset (Fin n)), H.IsUniform 3 ∧
      ¬ H.ContainsSubgraph 4 3 ∧ (2 / 7 - ε) * (n.choose 3 : ℝ) ≤ (H.card : ℝ) := by
…
```