Issues

• [Award claim] JSP-000649

  TheJustinSunPrize/awards#4702 · Filter by author JENW1N opened on Oct 5, 2026
  1

• [Problem] Recommend the Neggers–Stanley conjecture with a complete Lean counterexample

  TheJustinSunPrize/awards#4645 · Filter by author aznikline opened on Sep 30, 2026

• [Award claim] JSP-000239

  TheJustinSunPrize/awards#4636 · Filter by author neelsomani opened on Sep 30, 2026

• [Award claim] JSP-000327

  TheJustinSunPrize/awards#4635 · Filter by author neelsomani opened on Sep 30, 2026

• [Feedback] JSP-000216 Lean formalization progress (incomplete)

  TheJustinSunPrize/awards#4536 · Filter by author ddddddfsd opened on Sep 25, 2026

• [Feedback] PR #88 closure notice describes a different submission

  TheJustinSunPrize/awards#3809 · Filter by author qkkqk1234 opened on Sep 22, 2026
  3

• [Correction] JSP-000554 — description drops the "for almost all n" quantifier (source: Erdős #682)

  TheJustinSunPrize/awards#3342 · Filter by author pokrc opened on Sep 22, 2026

• [Correction] JSP-000947 — description drops the quantifier over n (source: Erdős #1142)

  TheJustinSunPrize/awards#3264 · Filter by author pokrc opened on Sep 22, 2026
  1

• [Correction] JSP-000876 — make the contiguity condition and the quantifier over k explicit in the problem description

  TheJustinSunPrize/awards#3263 · Filter by author pokrc opened on Sep 22, 2026
  1

• [Problem] Module 9: René Thom 1954 Cobordism Classification for 2-Manifolds

  TheJustinSunPrize/awards#2920 · Filter by author CreizyLabs opened on Sep 22, 2026

• [Problem] Module 10: Kirby-Taylor Mod-8 Pin⁻ Cobordism Invariant in ℤ[i]

  TheJustinSunPrize/awards#2919 · Filter by author CreizyLabs opened on Sep 22, 2026

• [Problem] Module 11: Poincaré Homology Sphere Boundary Topology and π₁ Obstruction

  TheJustinSunPrize/awards#2918 · Filter by author CreizyLabs opened on Sep 22, 2026

• [Problem] Module 12: Conway-Sloane E8 Minimal Root Quantization and Gosset 421 Polytope

  TheJustinSunPrize/awards#2917 · Filter by author CreizyLabs opened on Sep 22, 2026

• [Problem] Erdős-Straus Conjecture: Machine-Closed Modular Egyptian Fraction Sub-Families (mod 4)

  TheJustinSunPrize/awards#2916 · Filter by author CreizyLabs opened on Sep 22, 2026

• [Problem] Kaplansky Unit Conjecture Refutation

  TheJustinSunPrize/awards#2912 · Filter by author CreizyLabs opened on Sep 22, 2026

• [Problem] Frankl's Union-Closed Sets Conjecture: Variational Entropy Floor

  TheJustinSunPrize/awards#2913 · Filter by author CreizyLabs opened on Sep 22, 2026

• [Problem] The E8 4-Manifold Non-Smoothability Obstruction

  TheJustinSunPrize/awards#2911 · Filter by author CreizyLabs opened on Sep 22, 2026

• [Problem] I-sn-metrizability of regular spaces with sigma-HCP I-sn-networks

  TheJustinSunPrize/awards#2898 · Filter by author starhoo123 opened on Sep 22, 2026
  1

• [Problem] Unimodular Trace-Free Gravitational Decoupling of Vacuum Energy

  TheJustinSunPrize/awards#2812 · Filter by author CreizyLabs opened on Sep 21, 2026
  1

• [Problem] Exact Diophantine Ring Invariants in Quadratic Integer Ring Z[phi]

  TheJustinSunPrize/awards#2811 · Filter by author CreizyLabs opened on Sep 21, 2026
  1

• [Correction] JSP-001022: Lean proof is recorded as No; a complete verified formalization exists

  TheJustinSunPrize/awards#2722 · Filter by author AuraFamerCode opened on Sep 21, 2026
  1

• [Award claim] JSP-000766: MaxwellLaw arbitrary-graph formalization (pending review)

  TheJustinSunPrize/awards#2288 · Filter by author MaxwellLaw opened on Sep 21, 2026

• [Award claim] JSP-000078: MaxwellLaw arbitrary-graph formalization (pending review)

  TheJustinSunPrize/awards#2287 · Filter by author MaxwellLaw opened on Sep 21, 2026

• [Award claim] JSP-000906 — Lean formalization (early claim; PR #756 pending)

  TheJustinSunPrize/awards#2281 · Filter by author Li-Hongmin opened on Sep 21, 2026
  1

• [Award claim] JSP-000625 — Lean formalization (early claim; PR #757 pending)

  TheJustinSunPrize/awards#2282 · Filter by author Li-Hongmin opened on Sep 21, 2026
  1