Erdős Problem 330

Stream: Formal conjectures

[AYUSH DEBNATH]

I am tring to build the code but getting an error like this
/-

Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");

you may not use this file except in compliance with the License.

You may obtain a copy of the License at

https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software

distributed under the License is distributed on an "AS IS" BASIS,

WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

See the License for the specific language governing permissions and

limitations under the License.
-/

import FormalConjectures.Util.ProblemImports

/-!

Erdős Problem 330

Reference: erdosproblems.com/330
-/

namespace Erdos330

open Set

open scoped BigOperators

/-- Rep_h A h m means m is a sum of h elements of A. -/

def Rep_h (A : Set ℕ) (h m : ℕ) : Prop :=

∃ f : Fin h → ℕ, (∀ i, f i ∈ A) ∧ (∑ i : Fin h, f i) = m

/-- Integers not representable as a sum of h elements of A without using n. -/

def UnrepWithout (A : Set ℕ) (h n : ℕ) : Set ℕ :=

{m | ¬ Rep_h (A \ {n}) h m}

/-- Minimality built on top of Set.IsAsymptoticAddBasis. -/

def MinAsymptoticAddBasis (A : Set ℕ) (h : ℕ) : Prop :=

Set.IsAsymptoticAddBasis A h ∧

∀ n ∈ A, ¬ Set.IsAsymptoticAddBasis (A \ {n}) h

@[category research open, AMS 5 11]

theorem erdos_330_statement

(h : ℕ) (A : Set ℕ)

(h2 : 2 ≤ h)

(hmin : MinAsymptoticAddBasis A h)

(hden : Set.HasPosDensity A) :

∀ n ∈ A, Set.HasPosDensity (UnrepWithout A h n) := by

sorry

end Erdos330

[AYUSH DEBNATH]

@Moritz Firsching @Paul Lezeau
The code is correct but shows this error
function expected at
(A \ {n}).IsAsymptoticAddBasis
term has type
Prop

function expected at
A.IsAsymptoticAddBasis
term has type
Prop

[AYUSH DEBNATH]

How do I fix this?

[Notification Bot]

This topic was moved here from #Formal conjectures > Erdős Problem #330 by AYUSH DEBNATH.

[Moritz Firsching]

The error comes from the fact that you use Set.IsAsymptoticAddBasis instead of Set.IsAsymptoticAddBasisOfOrder

[Moritz Firsching]

Please read #backticks

[Moritz Firsching]

You can see the type of Set.IsAsymptoticAddBasis by hovering over it, or writing #check Set.IsAsymptoticAddBasis or right-click and click on "Go to definition".

[AYUSH DEBNATH]

/-

Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");

you may not use this file except in compliance with the License.

You may obtain a copy of the License at

https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software

distributed under the License is distributed on an "AS IS" BASIS,

WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

See the License for the specific language governing permissions and

limitations under the License.
-/

import FormalConjectures.Util.ProblemImports

/-!

Erdős Problem 330

Reference: erdosproblems.com/330
-/

namespace Erdos330

open Set

open scoped BigOperators

/-- Rep_h A h m means m is a sum of h elements of A. -/

def Rep_h (A : Set ℕ) (h m : ℕ) : Prop :=

∃ f : Fin h → ℕ, (∀ i, f i ∈ A) ∧ (∑ i : Fin h, f i) = m

/-- Integers not representable as a sum of h elements of A without using n. -/

def UnrepWithout (A : Set ℕ) (h n : ℕ) : Set ℕ :=

{m | ¬ Rep_h (A \ {n}) h m}

/-- Minimality built on Set.IsAsymptoticAddBasisOfOrder. -/

def MinAsymptoticAddBasis (A : Set ℕ) (h : ℕ) : Prop :=

Set.IsAsymptoticAddBasisOfOrder A h ∧

∀ n ∈ A, ¬ Set.IsAsymptoticAddBasisOfOrder (A \ {n}) h

@[category research open, AMS 5 11]

theorem erdos_330_statement

(h : ℕ) (A : Set ℕ)

(h2 : 2 ≤ h)

(hmin : MinAsymptoticAddBasis A h)

(hden : Set.HasPosDensity A) :

∀ n ∈ A, Set.HasPosDensity (UnrepWithout A h n) ↔ answer(sorry) := by

sorry

end Erdos330

Thanks here is my corrected code

[AYUSH DEBNATH]

Is it good to merge? @Moritz Firsching

[Moritz Firsching]

Let's do the code review in the pull request

[AYUSH DEBNATH]

Passed all the checks can we merge it now @Moritz Firsching