All pull requests

Pull requests

• feat(ErdosProblems/1191): add solved dyadic, Legendre-Fenchel, and Haar sawtooth variants with Lean proof links

  erdos-problems
  #7640·doublegate opened Oct 27, 2026·

  ·
  2

• feat(Wikipedia): formalize Cullen primes and the Cullen prime conjecture

  wikipedia
  #7639·Karansankhe opened Oct 27, 2026·

  ·

• feat(ErdosProblems/699): add solved variant for j^2 < n with Lean proof link

  erdos-problems
  #7637·Paulee314 opened Oct 27, 2026·

  ·

• feat(millennium): formalise 4D Yang-Mills Existence and Mass Gap conjecture

  millennium-problems
  #7636·Cloudhabil opened Oct 26, 2026·

  ·
  1

  1

• feat: add linter to enforce Palomar submissions

  attributesdocumentation
  #7631·Paul-Lez opened Oct 26, 2026Collaborator·

  ·
  1

• Mark Erdős 802 solved with verified Lean proof

  erdos-problems
  #7630·AItoBit opened Oct 26, 2026Contributor·

  ·

• Share definitions used by the Konamiu submissions

  erdos-problemsfor-mathlibmathoverflow
  #7629·Paul-Lez opened Oct 26, 2026Collaborator·

  ·

• feat(Arxiv/1912.12687): state Jesmanowicz' conjecture

  arxiv
  #7627·Qunsheng-Zhang opened Oct 26, 2026·

  ·
  1

• refactor(ErdosProblems/508): extract optimization constant 27a

  erdos-problems
  #7625·Qunsheng-Zhang opened Oct 26, 2026·

  ·
  2

• feat(ErdosProblems/962): link the Tao square-root upper bound proof

  erdos-problems
  #7624·linrock opened Oct 26, 2026Contributor·

  ·

• feat(ErdosProblems/661): link proof of Lenz's R^4 construction

  erdos-problems
  #7623·linrock opened Oct 26, 2026Contributor·

  ·

• feat(ErdosProblems/423): link Lean proofs for three solved variants

  erdos-problems
  #7622·linrock opened Oct 26, 2026Contributor·

  ·

• feat(ErdosProblems/968): link the Erdős–Prachar companion proofs

  erdos-problems
  #7621·linrock opened Oct 25, 2026Contributor·

  ·

• feat(ErdosProblems/338): link formal proof of the Hegyvári–Hennecart–Plagne variant

  erdos-problems
  #7620·linrock opened Oct 25, 2026Contributor·

  ·

• feat(ErdosProblems/501): link the Erdős–Hajnal finite independent-set proof

  erdos-problems
  #7619·linrock opened Oct 25, 2026Contributor·

  ·

• feat(SimpleGraph): add uniform graph proportions for Erdős 799

  for-mathlib
  #7617·AItoBit opened Oct 25, 2026Contributor·

  ·

• Add bundled acyclic vertex colorings and acyclic chromatic number

  for-mathlib
  #7616·AItoBit opened Oct 25, 2026Contributor·

  ·

• Share distinct subset sums/products API for Erdős 350 and 795

  erdos-problemsfor-mathlib
  #7615·AItoBit opened Oct 25, 2026Contributor·

  ·

• Mathoverflow 516372: extreme points of the 2×2 marginal body

  mathoverflow
  #7614·JarekDuda opened Oct 25, 2026·

  ·
  1

  2

• Add verified classical bounds for Erdős 792

  erdos-problems
  #7612·AItoBit opened Oct 25, 2026Contributor·

  ·

• feat(OpenQuantumProblems/35): formal proof link for the AME(7,d) classification

  open-quantum-problems
  #7611·zblore opened Oct 25, 2026Contributor·

  ·

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

  erdos-problems
  #7610·veljjanoski opened Oct 25, 2026Contributor·

  ·
  1

  2

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

  erdos-problems
  #7604·veljjanoski opened Oct 25, 2026Contributor·

  ·
  3

• feat(OpenQuantumProblems/23): mark SIC-POVM existence solved and link the formal proof

  open-quantum-problems
  #7600·Hertaspace opened Oct 25, 2026·

  ·
  2

• feat(ErdosProblems): formalize the negative asymptotic answer to problem 791

  erdos-problems
  #7599·AItoBit opened Oct 25, 2026Contributor·

  ·