diff --git a/LeanAPAP/Integer.lean b/LeanAPAP/Integer.lean
new file mode 100644
index 0000000000..65123147ef
--- /dev/null
+++ b/LeanAPAP/Integer.lean
@@ -0,0 +1,7 @@
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
+import Mathlib.Combinatorics.Additive.AP.Three.Defs
+
+open Finset Real
+
+theorem int {A : Finset ℕ} {N : ℕ} (hAN : A ⊆ range N) (hA : ThreeAPFree (α := ℕ) A) :
+    ∃ c > 0, A.card ≤ N / exp (- c * log N ^ (12⁻¹ : ℝ)) := sorry
diff --git a/blueprint/src/chapter/integers.tex b/blueprint/src/chapter/integers.tex
index cd534fff58..ce770bb664 100644
--- a/blueprint/src/chapter/integers.tex
+++ b/blueprint/src/chapter/integers.tex
@@ -122,12 +122,15 @@ \chapter{The integer case}
 To do.
 \end{proof}
 
-\begin{theorem}\label{3aps-in-ints}
-If $A\subseteq \{1,\ldots,N\}$ contains no non-trivial three-term arithmetic progressions then
-\[\lvert A\rvert \leq \frac{N}{\exp(-c(\log N)^{1/12})}\]
-for some constant $c>0$.
+\begin{theorem}[Integer case]
+  \label{int}
+  \uses{}
+  \lean{int}
+  \leanok
+  If $A\subseteq \{1,\ldots,N\}$ contains no non-trivial three-term arithmetic progressions then
+  \[\lvert A\rvert \leq \frac{N}{\exp(-c(\log N)^{1/12})}\]
 \end{theorem}
 \begin{proof}
 \uses{main-int-count}
-To do.
+  To do.
 \end{proof}