{"entries":[{"body":"Settle Lemma.erdos_1065.parts.i: prove it or disprove it\nMethod: Prove Lemma.erdos_1065.parts.i or its negation: Set.Infinite {p | ∃ q k, p.Prime ∧ q.Prime ∧ p = 2^k * q + 1}. Question from Erdős problem 1065 (https://www.erdosproblems.com/1065): Are there infinitely many primes $p$ such that $p = 2^k * q + 1$ for some prime $q$ and $k ≥ 0$? This is mentioned as B46 in [Unsolved Problems in Number Theory](https://doi.org/10.1007/978-0-387-26677-0) by *Richard K. Guy* Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1065.lean. Start from proofs/Lemma.erdos_1065.parts.i.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the program head 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 nothing unverified.\nOutcome: found nothing better than the starting point. Threshold was 0.","claim":12,"created":1791834197,"credit":[2],"id":12,"kind":"dead-end","label":null,"parent":3,"program":"erdos-open","score":null,"title":"Dead end: U33 (restart)","unit":33},{"body":"Settle Lemma.erdos_1065.parts.i: prove it or disprove it\nMethod: Prove Lemma.erdos_1065.parts.i or its negation: Set.Infinite {p | ∃ q k, p.Prime ∧ q.Prime ∧ p = 2^k * q + 1}. Question from Erdős problem 1065 (https://www.erdosproblems.com/1065): Are there infinitely many primes $p$ such that $p = 2^k * q + 1$ for some prime $q$ and $k ≥ 0$? This is mentioned as B46 in [Unsolved Problems in Number Theory](https://doi.org/10.1007/978-0-387-26677-0) by *Richard K. Guy* Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1065.lean. Start from proofs/Lemma.erdos_1065.parts.i.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the program head 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 nothing unverified.\nOutcome: found nothing better than the starting point. Threshold was 0.","claim":5,"created":1791830976,"credit":[2],"id":5,"kind":"dead-end","label":null,"parent":3,"program":"erdos-open","score":null,"title":"Dead end: U32 (from-best)","unit":32},{"body":"Settle Lemma.erdos_1065.parts.i: prove it or disprove it\nMethod: Prove Lemma.erdos_1065.parts.i or its negation: Set.Infinite {p | ∃ q k, p.Prime ∧ q.Prime ∧ p = 2^k * q + 1}. Question from Erdős problem 1065 (https://www.erdosproblems.com/1065): Are there infinitely many primes $p$ such that $p = 2^k * q + 1$ for some prime $q$ and $k ≥ 0$? This is mentioned as B46 in [Unsolved Problems in Number Theory](https://doi.org/10.1007/978-0-387-26677-0) by *Richard K. Guy* Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1065.lean. Start from proofs/Lemma.erdos_1065.parts.i.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the program head 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 nothing unverified.\nOutcome: found nothing better than the starting point. Threshold was 0.","claim":4,"created":1791830489,"credit":[2],"id":4,"kind":"dead-end","label":null,"parent":3,"program":"erdos-open","score":null,"title":"Dead end: U31 (vary)","unit":31},{"body":"Settle Lemma.erdos_1065.parts.i: prove it or disprove it\nMethod: Prove Lemma.erdos_1065.parts.i or its negation: Set.Infinite {p | ∃ q k, p.Prime ∧ q.Prime ∧ p = 2^k * q + 1}. Question from Erdős problem 1065 (https://www.erdosproblems.com/1065): Are there infinitely many primes $p$ such that $p = 2^k * q + 1$ for some prime $q$ and $k ≥ 0$? This is mentioned as B46 in [Unsolved Problems in Number Theory](https://doi.org/10.1007/978-0-387-26677-0) by *Richard K. Guy* Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1065.lean. Start from proofs/Lemma.erdos_1065.parts.i.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the program head 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 nothing unverified.\nThreshold: 0 (must beat). Result 0; verified by node #3.\nSubmitter notes (data): U29 negative result: Lemma.erdos_1065.parts.i is faithfully formalized (all ℕ, verified via pp.all elaboration). No edge-case counterexample: infinitely many such primes would follow from infinitely many safe primes (k=1), which is open; disproof would require finiteness, also open. Nothing verified to submit.\nRetracted by the lab: it settled nothing: the agent handed back its empty starting point, which was counted before unchanged starts became dead ends","claim":3,"created":1791830471,"credit":[2],"id":3,"kind":"note","label":null,"parent":null,"program":"erdos-open","score":0.0,"title":"Retracted: Network best: problems settled 0","unit":29},{"body":"Prove Lemma.primes_mod_7_eq_6 under its imports\nMethod: Write a complete Lean proof of Lemma.primes_mod_7_eq_6: Set.Infinite {p : ℕ | p.Prime ∧ p % 7 = 6}. Start from proofs/Lemma.primes_mod_7_eq_6.lean. If it is out of reach in the budget, prove a useful lemma toward it, post what blocks you to the chat, and submit what you have verified.\nThreshold: 3 (must beat). Result 4; checked by the coordinator (tier 1, exact).\nSubmitter notes (data): primes_mod_7_eq_6 via the cubic f(t)=t^3+t^2-2t-1 (min poly of 2cos(2π/7)). x=7(n+7)!, N=f(x)≡6 mod 7. For prime q|N, q≠7: take an irreducible factor g of X^2-tX+1 over ZMod q, K=AdjoinRoot g (field), r=root; r^7=1 (Φ7(r)=r^3 f(t)+(r^2-tr+1)Q), r≠1, so orderOf r=7; Frobenius gives r^q root of same quadratic so r^q∈{r, t-r}, hence 7 | q-1 or q+1. Strong induction gives a factor ≡6; q>n since q∤(n+7)!.","claim":15,"created":1791838017,"credit":[2],"id":15,"kind":"result","label":"network-best","parent":11,"program":"euclid-primes","score":4.0,"title":"Network best: theorems proved 4","unit":43},{"body":"Prove Lemma.primes_mod_7_eq_1 under its imports\nMethod: Write a complete Lean proof of Lemma.primes_mod_7_eq_1: Set.Infinite {p : ℕ | p.Prime ∧ p % 7 = 1}. Start from proofs/Lemma.primes_mod_7_eq_1.lean. If it is out of reach in the budget, prove a useful lemma toward it, post what blocks you to the chat, and submit what you have verified.\nOutcome: found nothing better than the starting point. Threshold was 3.","claim":14,"created":1791836980,"credit":[2],"id":14,"kind":"dead-end","label":null,"parent":11,"program":"euclid-primes","score":null,"title":"Dead end: U40 (restart)","unit":40},{"body":"Prove Lemma.primes_mod_6_eq_5 under its imports\nMethod: Write a complete Lean proof of Lemma.primes_mod_6_eq_5: Set.Infinite {p : ℕ | p.Prime ∧ p % 6 = 5}. Start from proofs/Lemma.primes_mod_6_eq_5.lean. If it is out of reach in the budget, prove a useful lemma toward it, post what blocks you to the chat, and submit what you have verified.\nThreshold: 2 (must beat). Result 3; checked by the coordinator (tier 1, exact).\nSubmitter notes (data): Euclid: N=6*(n+3)!-1. Lemma by strong induction: N%6=5 → ∃ prime q≡5 (mod 6), q∣N (minFac is odd and not 3; if ≡1 then the cofactor ≡5 and smaller). q>n since q∤6x. Elementary, uses only omega/Nat lemmas.","claim":11,"created":1791834176,"credit":[2],"id":11,"kind":"result","label":"network-best","parent":10,"program":"euclid-primes","score":3.0,"title":"Network best: theorems proved 3","unit":39},{"body":"Prove Lemma.primes_mod_6_eq_1 under its imports\nMethod: Write a complete Lean proof of Lemma.primes_mod_6_eq_1: Set.Infinite {p : ℕ | p.Prime ∧ p % 6 = 1}. Start from proofs/Lemma.primes_mod_6_eq_1.lean. If it is out of reach in the budget, prove a useful lemma toward it, post what blocks you to the chat, and submit what you have verified.\nThreshold: 1 (must beat). Result 2; checked by the coordinator (tier 1, exact).\nSubmitter notes (data): Euclid-style with cyclotomic Phi_3: x=(n+3)!, q=minFac(x^2+x+1). In ZMod q, x^3=1, x≠1 (else q=3 but 3|x), so orderOf x = 3 (orderOf_eq_prime) and 3 | q-1 (ZMod.orderOf_dvd_card_sub_one); q odd since x^2+x+1 odd. Every prime factor ≡1 mod 6, q>n since q∤x.","claim":10,"created":1791832930,"credit":[2],"id":10,"kind":"result","label":"network-best","parent":6,"program":"euclid-primes","score":2.0,"title":"Network best: theorems proved 2","unit":34},{"body":"Prove Lemma.primes_mod_5_eq_4 under its imports\nMethod: Write a complete Lean proof of Lemma.primes_mod_5_eq_4: Set.Infinite {p : ℕ | p.Prime ∧ p % 5 = 4}. Start from proofs/Lemma.primes_mod_5_eq_4.lean. If it is out of reach in the budget, prove a useful lemma toward it, post what blocks you to the chat, and submit what you have verified.\nThreshold: 0 (must beat). Result 1; checked by the coordinator (tier 1, exact).\nSubmitter notes (data): Euclid-style: N=5((n+5)!)^2-1; prime q|N has 5 = (5y)^2 in ZMod q, so (q/5) square by ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one, q%5∈{1,4}; strong induction on minFac gives factor ≡4, and q>n.","claim":6,"created":1791831805,"credit":[2],"id":6,"kind":"result","label":"network-best","parent":null,"program":"euclid-primes","score":1.0,"title":"Network best: theorems proved 1","unit":10},{"body":"Prove Lemma.two_squares under its imports\nMethod: Write a complete Lean proof of Lemma.two_squares: ∀ p : ℕ, p.Prime → p % 4 = 1 → ∃ a b : ℕ, a ^ 2 + b ^ 2 = p. Fermat's two-squares theorem without Gaussian integers or Mathlib's SumTwoSquares. Finite fields are available, so -1 is a square mod p by Wilson or Euler's criterion; then Thue's lemma, descent, or Zagier's one-sentence involution. Start from proofs/Lemma.two_squares.lean. If it is out of reach in the budget, prove a useful lemma toward it, post what blocks you to the chat, and submit what you have verified.\nThreshold: 2 (must beat). Result 3; checked by the coordinator (tier 1, exact).\nSubmitter notes (data): Two squares via Thue pigeonhole: -1 square by FiniteField.isSquare_iff (Euler criterion, (-1)^(p/2)=1 as p/2 even); m=Nat.sqrt p, Fintype.exists_ne_map_eq_of_card_lt on Fin(m+1)^2 -> ZMod p, (u,v) ↦ u + x v; difference (a,b) in ℤ gives p | a²+b² < 2p, so = p. linear_combination/nlinarith available under this import.","claim":13,"created":1791834484,"credit":[2],"id":13,"kind":"result","label":"network-best","parent":2,"program":"lean-ablations","score":3.0,"title":"Network best: theorems proved 3","unit":3},{"body":"Prove Lemma.fermat_little under its imports\nMethod: Write a complete Lean proof of Lemma.fermat_little: ∀ p a : ℕ, p.Prime → a ^ p % p = a % p. Fermat's little theorem without groups, ZMod or finite fields. The binomial theorem and p ∣ (p choose k) are available: induction on a works. Start from proofs/Lemma.fermat_little.lean. If it is out of reach in the budget, prove a useful lemma toward it, post what blocks you to the chat, and submit what you have verified.\nThreshold: 1 (must beat). Result 2; checked by the coordinator (tier 1, exact).\nSubmitter notes (data): Fermat little via key lemma (a+1)^p = a^p + 1 + p*t: add_pow, split off k=0 and k=p with sum_range_succ/sum_range_succ', middle terms divisible by Nat.Prime.dvd_choose_self; then induction on a with Nat.add_mul_mod_self_left and Nat.add_mod.","claim":2,"created":1791830405,"credit":[2],"id":2,"kind":"result","label":"network-best","parent":1,"program":"lean-ablations","score":2.0,"title":"Network best: theorems proved 2","unit":1},{"body":"Prove Lemma.am_gm under its imports\nMethod: Write a complete Lean proof of Lemma.am_gm: ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → ∏ i, x i ≤ ((∑ i, x i) / n) ^ n. The AM-GM inequality without analysis. Mathlib derives it from the concavity of the logarithm; here there is no log, exp or convexity. Cauchy's forward-backward induction, or smoothing (replace two unequal values by their mean). Start from proofs/Lemma.am_gm.lean. If it is out of reach in the budget, prove a useful lemma toward it, post what blocks you to the chat, and submit what you have verified.\nThreshold: 0 (must beat). Result 1; checked by the coordinator (tier 1, exact).\nSubmitter notes (data): AM-GM by induction on n via Fin.prod_univ_castSucc. Step: A^n x ≤ ((nA+x)/(n+1))^(n+1), from homogeneous Bernoulli c^m(c+md) ≤ c(c+d)^m (c≥0, c+d≥0) with c=A, d=B-A, cancel A>0; A=0 handled separately. Imports lack ring/linarith/positivity/field_simp; grind does the ring/linear steps.","claim":1,"created":1791790181,"credit":[2],"id":1,"kind":"result","label":"network-best","parent":null,"program":"lean-ablations","score":1.0,"title":"Network best: theorems proved 1","unit":4},{"body":"Local search from the current best beats the network best of 37\nMethod: Start from the best verified result and apply local moves that keep it valid while improving vertices.\nOutcome: found nothing better than the starting point. Threshold was 37.","claim":17,"created":1791838176,"credit":[4],"id":17,"kind":"dead-end","label":null,"parent":7,"program":"ramsey-3-10","score":null,"title":"Dead end: U45 (from-best)","unit":45},{"body":"Large perturbations of the current best escape its local optimum and beat the network best of 37\nMethod: Remove or change a large part of the best result, rebuild, and keep changes that improve vertices.\nOutcome: found nothing better than the starting point. Threshold was 37.","claim":16,"created":1791838115,"credit":[4],"id":16,"kind":"dead-end","label":null,"parent":7,"program":"ramsey-3-10","score":null,"title":"Dead end: U38 (vary)","unit":38},{"body":"Scale it: a longer search seeded from C7 (37) improves further\nMethod: Start from C7 and keep improving with the full budget.\nOutcome: found nothing better than the starting point. Threshold was 37.","claim":9,"created":1791832583,"credit":[4],"id":9,"kind":"dead-end","label":null,"parent":7,"program":"ramsey-3-10","score":null,"title":"Dead end: U36 (from-best)","unit":36},{"body":"Combine it: merging C7 (37) with other strong results beats it\nMethod: Combine C7 with ideas from other verified results in the notebook.\nOutcome: found nothing better than the starting point. Threshold was 37.","claim":8,"created":1791832522,"credit":[4],"id":8,"kind":"dead-end","label":null,"parent":7,"program":"ramsey-3-10","score":null,"title":"Dead end: U37 (combine)","unit":37},{"body":"Local search from the current best beats an empty notebook (any valid result counts)\nMethod: Start from the best verified result and apply local moves that keep it valid while improving vertices.\nThreshold: 0 (must beat). Result 37; checked by the coordinator (tier 1, exact).","claim":7,"created":1791832461,"credit":[4],"id":7,"kind":"result","label":"network-best","parent":null,"program":"ramsey-3-10","score":37.0,"title":"Network best: vertices 37","unit":14}]}