refactor(erdos-1107): use Nat.Full, add filter notation and Heath-Bro…

…wn variant

Address code review feedback from @mo271:
- Replaced local `IsRPowerful` definition with `Nat.Full` imported from `ForMathlib`.
- Refactored the summation property into a helper `SumOfRPowerful` to avoid code duplication.
- Switched to filter notation (`∀ᶠ n in atTop`) to correctly capture the "every large integer" condition.
- Added `erdos_1107.variants.two` to formally state the solved case for r=2 (Heath-Brown, 1988).
- Updated docstrings and tags (added `solved` to the variant).

FormalConjectures/ErdosProblems/1107.lean

@@ -15,31 +15,41 @@ limitations under the License.
 -/
 
 import FormalConjectures.Util.ProblemImports
+import FormalConjectures.ForMathlib.Data.Nat.Full
 
 /-!
 # Erdős Problem 1107
 
 *Reference:* [erdosproblems.com/1107](https://www.erdosproblems.com/1107)
+
+Every large integer is the sum of at most $r+1$ many $r$-powerful numbers.
+proved by Heath-Brown [He88] for $r=2$ (sums of 3 square-full numbers).
+
+[He88] Heath-Brown, D. R., Ternary quadratic forms and sums of three square-full numbers. (1988)
 -/
 
 namespace Erdos1107
 
-open Nat
+open Nat Filter
 
 /--
-A number $n$ is $r$-powerful if for every prime $p$ which divides $n$,
-we have $p^r$ divides $n$.
+Helper Property: $n$ is the sum of at most $r+1$ numbers, each of which is $r$-full.
 -/
-def IsRPowerful (r n : ℕ) : Prop :=
-  ∀ p, p.Prime → p ∣ n → p ^ r ∣ n
+def SumOfRPowerful (r n : ℕ) : Prop :=
+  ∃ s : List ℕ, s.length ≤ r + 1 ∧ (∀ x ∈ s, Nat.Full r x) ∧ s.sum = n
 
 /--
 Let $r \ge 2$. Is every large integer the sum of at most $r + 1$ many $r$-powerful numbers?
 -/
 @[category research open, AMS 11]
-theorem erdos_1107 :
-    ∀ r ≥ 2, ∃ N, ∀ n ≥ N,
-    ∃ s : List ℕ, s.length ≤ r + 1 ∧ (∀ x ∈ s, IsRPowerful r x) ∧ s.sum = n := by
+theorem erdos_1107 : ∀ r ≥ 2, ∀ᶠ n in atTop, SumOfRPowerful r n := by
+  sorry
+
+/--
+Heath-Brown [He88] proved this for $r=2$.
+-/
+@[category research solved, AMS 11]
+theorem erdos_1107.variants.two : ∀ᶠ n in atTop, SumOfRPowerful 2 n := by
   sorry
 
 end Erdos1107