From e026f0a0f81ac2e5ad76fe725786538cdfaf2c82 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Wed, 23 Sep 2026 16:09:06 +0800
Subject: [PATCH] feat(NumberTheory): Sylvester's conjecture

---
 LeanEval/NumberTheory/Sylvester.lean | 25 +++++++++++++++++++++++++
 manifests/problems/sylvester.toml    | 15 +++++++++++++++
 2 files changed, 40 insertions(+)
 create mode 100644 LeanEval/NumberTheory/Sylvester.lean
 create mode 100644 manifests/problems/sylvester.toml

diff --git a/LeanEval/NumberTheory/Sylvester.lean b/LeanEval/NumberTheory/Sylvester.lean
new file mode 100644
index 000000000..6b4ba3b86
--- /dev/null
+++ b/LeanEval/NumberTheory/Sylvester.lean
@@ -0,0 +1,25 @@
+import Mathlib
+import EvalTools.Markers
+
+/-!
+# Sylvester's conjecture
+
+Every prime number congruent to 4, 7 or 8 modulo 9 is the sum of two rational cubes.
+In fact squares of such primes are also the sum of two rational cubes.
+The proof uses Heegner points and Rankin–Selberg L-functions.
+
+## References
+
+* Hongbo Yin. A proof of the 4,7 cases of Sylvester’s conjecture on cube sums. https://arxiv.org/abs/2605.25917
+* Ashay Burungale, Ye Tian. A proof of Sylvester's conjecture. https://arxiv.org/abs/2609.14893
+* http://arxiv.org/abs/2304.09806 is an earlier but problematic claim, see https://x.com/samit_dasgupta/status/2100283036088606910.
+-/
+
+namespace LeanEval.NumberTheory
+
+@[eval_problem]
+theorem sylvester (p : ℕ) (h : p.Prime) (h' : p % 9 ∈ ({4, 7, 8} : Set ℕ)) :
+    (∃ a b : ℚ, p = a ^ 3 + b ^ 3) ∧ (∃ a b : ℚ, p ^ 2 = a ^ 3 + b ^ 3) := by
+  sorry
+
+end LeanEval.NumberTheory
diff --git a/manifests/problems/sylvester.toml b/manifests/problems/sylvester.toml
new file mode 100644
index 000000000..702f2de32
--- /dev/null
+++ b/manifests/problems/sylvester.toml
@@ -0,0 +1,15 @@
+id = "sylvester"
+title = "Sylvester's conjecture"
+group = "formalization-evaluation"
+status = "active"
+visible = true
+statement_revision = 1
+tags = []
+module = "LeanEval.NumberTheory.Sylvester"
+holes = ["sylvester"]
+submitter = "Junyan Xu"
+
+[[status_history]]
+status = "active"
+effective_date = "2026-09-23"
+reason = "policy"