All pull requests

Pull requests

• feat(ErdosProblems/23): prove n1, n5_tight and blowupC5_tight

  erdos-problems
  #6873·bengoechea opened Oct 5, 2026Contributor·

  ·

• feat(ErdosProblems/698): prove the Erdős–Szekeres gcd bound and its sharp case

  erdos-problems
  #6872·bengoechea opened Oct 5, 2026Contributor·

  ·

• feat(ErdosProblems/865): prove the k = 2 folklore case

  erdos-problems
  #6871·bengoechea opened Oct 5, 2026Contributor·

  ·

• feat(ForMathlib/Density, ErdosProblems/1136, 1193): density of multiples; prove three solved variants

  erdos-problemsfor-mathlib
  #6870·bengoechea opened Oct 5, 2026Contributor·

  ·

• Add review reports and evaluation harness separately from the skill

  CIdocumentation
  #6869·williamjblair opened Oct 5, 2026Collaborator·

  ·

• feat(ErdosProblems): formalize problem 338 with examples

  erdos-problems
  #6868·AItoBit opened Oct 5, 2026Contributor·

  ·
  1

• feat(ErdosProblems): formalize problem 336

  erdos-problems
  #6867·AItoBit opened Oct 5, 2026Contributor·

  ·
  1

• feat(ErdosProblems): add 335 statements and periodic examples

  erdos-problems
  #6866·AItoBit opened Oct 5, 2026Contributor·

  ·
  2

• feat(ErdosProblems): add 334 with smooth-sum bounds

  erdos-problemsfor-mathlib
  #6865·AItoBit opened Oct 5, 2026Contributor·

  ·
  1

• feat(ErdosProblems/687): add Erdős Problem 687

  erdos-problems
  #6864·veljjanoski opened Oct 5, 2026·

  ·
  1

• feat(ErdosProblems/554): add Erdős Problem 554

  erdos-problems
  #6863·veljjanoski opened Oct 5, 2026·

  ·
  1

• feat(ErdosProblems/420): add Erdős Problem 420

  erdos-problems
  #6862·veljjanoski opened Oct 5, 2026·

  ·
  1

• feat(ErdosProblems/408): add Erdős Problem 408

  erdos-problems
  #6861·veljjanoski opened Oct 5, 2026·

  ·
  1

• feat(ErdosProblems/393): add Erdős Problem 393

  erdos-problems
  #6860·veljjanoski opened Oct 5, 2026·

  ·
  1

• feat(ErdosProblems): formalise 327 with elementary bounds

  erdos-problemsfor-mathlib
  #6859·AItoBit opened Oct 5, 2026Contributor·

  ·
  1

• Formalize q-permanent Conjectures 1 and 2 and record their disproofs

  arxiv
  #6857·KitaKen1 opened Oct 5, 2026Contributor·

  ·

• feat(OEIS): add A000136 stamp folding growth rate conjecture

  oeis
  #6856·akanil18 opened Oct 4, 2026Contributor·

  ·
  1

  1

• feat(ErdosProblems): add 311 with gap bounds and formulation equivalence

  erdos-problemsfor-mathlib
  #6855·AItoBit opened Oct 4, 2026Contributor·

  ·

• feat(Wikipedia/LovaszPlummerConjecture): formal proof of the Lovász–Plummer conjecture

  wikipedia
  #6854·anatoliiohorodnyk opened Oct 4, 2026Contributor·

  ·
  1

• fix(ErdosProblems/1207): record the planar isosceles-free bound

  erdos-problems
  #6852·anxkhn opened Oct 4, 2026·

  ·
  1

• fix(ErdosProblems/1133): record the robust interpolation solution

  erdos-problems
  #6851·anxkhn opened Oct 4, 2026·

  ·
  1

• fix(ErdosProblems/413): mark weak omega barriers solved

  erdos-problems
  #6850·anxkhn opened Oct 4, 2026·

  ·
  1

• fix(ErdosProblems/348): record the deletion classification

  erdos-problems
  #6849·anxkhn opened Oct 4, 2026·

  ·
  1

• fix(ErdosProblems/270): record the solved linear case

  erdos-problems
  #6848·anxkhn opened Oct 4, 2026·

  ·
  1

• docs(Wikipedia/Pell): document the initial-value tests

  wikipedia
  #6847·anxkhn opened Oct 4, 2026·

  ·