All pull requests

Pull requests

• fix(ErdosProblems/1054): erdos_1054.parts.i is false

  erdos-problems
  #6760·ashm1tr opened Sep 30, 2026·

  ·

• feat(OEIS/51903): answer conjecture2 (False) and conjecture3 (True) with formal proofs

  oeis
  #6759·anshM123 opened Sep 30, 2026·

  ·

• Erdős Problem 176: statements, and proofs of the N(k, 2) and N(k, c√k) (c < 1) questions

  erdos-problems
  #6758·AItoBit opened Sep 30, 2026Contributor·

  ·

• feat(ErdosProblems): 177

  erdos-problems
  #6756·AItoBit opened Sep 30, 2026Contributor·

  ·

• fix(ErdosProblems/1046): erdos_1046.variants.diameter is true

  erdos-problemssolution found
  #6755·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(GreensOpenProblems/14): W_3_29_eq and W_3_30_eq are false

  green-problemssolution found
  #6754·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/1106): erdos_1106.parts.i is true

  erdos-problemssolution found
  #6753·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/968): the increasing and decreasing triple variants are true

  erdos-problemssolution found
  #6752·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/80): erdos_80.parts.i is false

  erdos-problemssolution found
  #6751·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/44): erdos_44.variants.empty_start is true

  erdos-problemssolution found
  #6750·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/331): erdos_331.variants.ruzsa is true

  erdos-problemssolution found
  #6749·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(GreensOpenProblems/1): green_1 is true

  green-problemssolution found
  #6748·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/319): answer erdos_319.variants.isTheta with fun N ↦ N

  erdos-problemssolution found
  #6747·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/1099): mark the factorial and lcm variants as solved

  erdos-problemssolution found
  #6746·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/184): erdos_184.variants.covering is true

  erdos-problemssolution found
  #6745·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/357): mark erdos_357.variants.hegyvari as solved

  erdos-problemssolution found
  #6744·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/1084): mark erdos_1084.variants.triangular_optimal_d2 as solved

  erdos-problemssolution found
  #6743·mo271 opened Sep 30, 2026Collaborator·

  ·

• fix(ErdosProblems/1095): mark erdos_1095.variants.upper_conjecture as solved

  erdos-problemssolution found
  #6742·mo271 opened Sep 30, 2026Collaborator·

  ·

• Formalize Littlewood's cylinder conjecture and mark as solved

  arxivBooks
  #6741·KitaKen1 opened Sep 30, 2026Contributor·

  ·

• chore: tag every yes-or-no question with the question attribute

  #6740·mo271 opened Sep 30, 2026Collaborator·

  ·

• feat(Util): add the question attribute

  attributesCIdocumentationlinter
  #6692·mo271 opened Sep 30, 2026Collaborator·

  ·

• feat(Books/Bugeaud): Problems 10.17 and 18 (solved)

  Booksfor-mathlib
  #6691·rwst opened Sep 30, 2026Contributor·

  ·

• chore(ErdosProblems): put answer(sorry) on the left of the iff

  erdos-problems
  #6689·mo271 opened Sep 30, 2026Collaborator·Queued

• Add the Courtade–Kumar conjecture (Paper/CourtadeKumar.lean)

  paper
  #6688·dpwoodru opened Sep 30, 2026·

  ·
  1

  1

• feat(ErdosProblems): add Erdős Problem 173

  erdos-problems
  #6686·AItoBit opened Sep 30, 2026Contributor·

  ·