All pull requests

Pull requests

• JSP-000301: record Lean formalization (scks1/jsp-000301-formalization)

  #5134·scks1 opened Oct 25, 2026·6 of 7 tasks·

  ·

• JSP-000938: record sharp first-order Lagrange interpolation asymptotics

  #5133·yuiyuiui opened Oct 24, 2026·3 of 4 tasks·

  ·

• JSP-000301: Lean formalization of the powerful-consecutive-integers disproof

  #5132·cosmos2explorer opened Oct 23, 2026·6 of 7 tasks·

  ·

• JSP-000404: sorry-free partial Lean formalization (exact alpha(N) for N<=8, sharpness for all N, full classification modulo one stated hypothesis)

  #5131·aznikline opened Oct 23, 2026·5 tasks done·

  ·

• JSP-000001: Riemann hypothesis Machine proof

  #5129·Shinsuke-Hamaji opened Oct 22, 2026·7 tasks done·

  ·

• JSP-000008: Goldbach conjecture (strong Goldbach) Machine Proof

  #5128·Shinsuke-Hamaji opened Oct 22, 2026·7 tasks done·

  ·

• JSP-000941: Collatz conjecture Machine proof

  #5127·Shinsuke-Hamaji opened Oct 22, 2026·7 tasks done·

  ·

• JSP-000301: record Lean formalization

  #5117·WK-Luo opened Oct 19, 2026·6 of 7 tasks·

  ·

• JSP-000907: record Lean formalization source (Erdos #1091 / Theorem 4.1)

  #5113·aujurd22 opened Oct 19, 2026·6 of 7 tasks·

  ·

• JSP-000012: Machine Proof of Legendre's Conjecture in Lean 4

  #5111·Shinsuke-Hamaji opened Oct 19, 2026·7 tasks done·

  ·
  1

• JSP-000785: original Kruer-Kohlmeyer solution and Lean proof

  #5110·lkruer opened Oct 19, 2026·7 tasks done·

  ·

• claim(JSP-000197): Complete Mathematical Solution and Kernel-Verified Lean 4 Proof for Planar Integral-Distance Points (Erdos-Anning) by CreizyLabs

  #5109·CreizyLabs opened Oct 18, 2026·7 tasks done·

  ·
  1

• claim(JSP-000148): Complete Mathematical Solution and Kernel-Verified Lean 4 Proof for Distinct Unit-Fraction Representations of One by CreizyLabs

  #5108·CreizyLabs opened Oct 18, 2026·7 tasks done·

  ·
  1

• JSP-000595: partial k=1 factorial divisibility; k>=2 unproved

  #5107·xccElephant opened Oct 18, 2026·

  ·
  1

• JSP-000579: unconditional parts.ii proved; uniform upper-bound question still open

  #5106·xccElephant opened Oct 18, 2026·1 of 3 tasks·

  ·
  1

• JSP-000072: partial formalization of Sidon constructions and conditional bounds

  #5105·xccElephant opened Oct 18, 2026·3 tasks·

  ·
  1

• JSP-000340: partial formalization of barrier dynamics and a conditional reduction

  #5104·xccElephant opened Oct 18, 2026·3 tasks·

  ·
  1

• JSP-000210: full eventual logarithmic runs for c2 < 2; general case remains open

  #5103·xccElephant opened Oct 18, 2026·1 of 3 tasks·

  ·
  1

• JSP-000533: partial formalization of the Straus isosceles-free construction

  #5102·xccElephant opened Oct 18, 2026·3 tasks·

  ·
  1

• JSP-000542: partial formalization of the four-point unit-distance classification

  #5101·xccElephant opened Oct 18, 2026·3 tasks·

  ·
  1

• JSP-000483: partial formalization of the C4-free countable escape variant

  #5100·xccElephant opened Oct 18, 2026·3 tasks·

  ·
  1

• JSP-000226: arbitrarily many finite choices of canonical representations; main gaps retained

  #5099·xccElephant opened Oct 18, 2026·1 of 3 tasks·

  ·
  1

• JSP-000234: partial p>=3 covering; original p>=5 problem unproved

  #5098·xccElephant opened Oct 18, 2026·

  ·
  1

• JSP-000546: complete four-term square-product theorem; general problem still open

  #5097·xccElephant opened Oct 18, 2026·1 of 3 tasks·

  ·
  1

• JSP-000395: partial formalization of restricted multiples-density bounds

  #5096·xccElephant opened Oct 18, 2026·3 tasks·

  ·
  1