{"claim":{"bundle":{"code":"","commit":"5012cc4ffcc28d370afdac4b45a211018ad2413f","config":null,"environment":"lemma/0.7.8 agent","logs":"","seeds":[]},"candidate":{"proofs":{}},"flags":[],"id":46,"lab_check":false,"label":null,"measured":null,"reason":"no improvement over the starting point","score":0.0,"significance":[],"status":"duplicate","verdicts":[]},"entry":{"body":"Settle Lemma.erdos_1158: prove it or disprove it\nMethod: Prove Lemma.erdos_1158 or its negation: ∀ t r : ℕ, 2 ≤ t → 2 ≤ r → ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ ((t : ℝ) - (r : ℝ) ^ (1 - (t : ℝ)) - ε) ≤ (Hypergraph.partiteExtremalNumber n t r : ℝ). Question from Erdős problem 1158 (https://www.erdosproblems.com/1158): Let $K_{t}(r)$ be the complete $t$-partite $t$-uniform hypergraph with $r$ vertices in each class. Is it true that $$\\mathrm{ex}_t(n,K_t(r)) \\geq n^{t-r^{1-t}-o(1)}$$ for all $t,r\\geq 2$? The restriction $r\\geq 2$ excludes forbidding a single edge. Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1158.lean. Start from proofs/Lemma.erdos_1158.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the lab's maintainers will report it upstream; say so in your notes. If neither is in reach, prove a useful special case or lemma, post what blocks you to the chat, and submit the files you started from unchanged, with notes on what you tried and what blocked you: the notebook keeps them as a dead end so others don't repeat it.\nOutcome: found nothing better than the starting point. Threshold was 0.\nSubmitter notes (data): U80 dead end for Lemma.erdos_1158. Printed definitions with #guard_msgs: partiteExtremalNumber n t r = extremalNumber n t (fun H => ¬ H.ContainsCompletePartiteHypergraph t r), extremalNumber = sup of card over subfamilies of powersetCard t univ (Fin n) satisfying P; ContainsCompletePartiteHypergraph H t r = ∃ f : Fin t × Fin r ↪ V, ∀ a : Fin t → Fin r, image (i ↦ f(i, a i)) ∈ H. This is exactly ex_t(n, K_t(r)), so the statement is faithful, with no edge case (t,r ≥ 2, eventually in n). The t=2 case is Zarankiewicz's ex(n,K_{r,r}) ≥ n^{2-1/r-o(1)}, which is open for r ≥ 4, so the full statement is open. I did not attempt formalizing the probabilistic deletion bound n^{t-(rt-t)/(r^t-1)} because it does not reach the conjectured exponent. Submitting the starting files unchanged.\nStatement checked: faithful\nBlocked by: out-of-reach\nWould unblock it: The t=2 case alone is the lower bound ex(n,K_{r,r}) ≥ n^{2-1/r-o(1)}, which is open for r≥4 (Kollár–Rónyai–Szabó and Bukh only cover unbalanced K_{s,t}), so a proof needs new constructions for the Erdős box problem; a disproof would need to improve the known upper bounds, which is also open.","claim":46,"created":1791914216,"credit":[2],"id":63,"kind":"dead-end","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Dead end: U80 (restart)","unit":80},"followups":[]}