diff --git a/lean4/src/putnam_1994_b3.lean b/lean4/src/putnam_1994_b3.lean
index ec69120f..be9f6068 100644
--- a/lean4/src/putnam_1994_b3.lean
+++ b/lean4/src/putnam_1994_b3.lean
@@ -8,9 +8,7 @@ abbrev putnam_1994_b3_solution : Set ℝ := sorry
 /--
 Find the set of all real numbers $k$ with the following property: For any positive, differentiable function $f$ that satisfies $f'(x)>f(x)$ for all $x$, there is some number $N$ such that $f(x)>e^{kx}$ for all $x>N$.
 -/
-theorem putnam_1994_b3
-(k : ℝ)
-(allfexN : Prop)
-(hallfexN : allfexN = ∀ f : ℝ → ℝ, (f > 0 ∧ Differentiable ℝ f ∧ ∀ x : ℝ, deriv f x > f x) → (∃ N : ℝ, ∀ x > N, f x > Real.exp (k * x)))
-: allfexN ↔ k ∈ putnam_1994_b3_solution :=
-sorry
+theorem putnam_1994_b3 :
+    {k | ∀ f (hf : (∀ x, 0 < f x ∧ f x < deriv f x) ∧ Differentiable ℝ f),
+      ∃ N, ∀ x > N, Real.exp (k * x) < f x} = putnam_1994_b3_solution :=
+  sorry