All pull requests

Pull requests

• 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·

  ·

• 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·

  ·

• JSP-000595: partial formalization of the k=1 factorial-divisibility variant

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

  ·

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

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

  ·

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

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

  ·

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

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

  ·

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

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

  ·

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

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

  ·

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

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

  ·

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

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

  ·

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

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

  ·

• JSP-000234: partial formalization of the p-at-least-3 covering variant

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

  ·

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

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

  ·

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

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

  ·

• JSP-000736: partial formalization of small-k common factor differences

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

  ·

• JSP-000569: partial formalization of binomial common-prime bounds

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

  ·

• JSP-000280: partial formalization of the Bateman restricted-basis counterexample

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

  ·

• JSP-000244: partial formalization of reciprocal-denominator gap bounds

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

  ·

• JSP-000058: partial formalization of the five-vertex edge-deletion case

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

  ·

• JSP-000781: infinite powerful-sum families for every r >= 6; remaining cases open

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

  ·

• JSP-000780: formalize infinite 3-powerful triples; scope unresolved

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

  ·

• JSP-000131: formalize the k=0 digit-representation result; scope unresolved

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

  ·

• JSP-000544: partial formalization of one-dimensional and conditional diameter bounds

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

  ·

• JSP-000489: partial formalization of countable-family property B

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

  ·