diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 8067c4c848..77bb3294d3 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -73,3 +73,27 @@ instance : HasToString Float := ⟨Float.toString⟩
 
 abbrev Nat.toFloat (n : Nat) : Float :=
 Float.ofNat n
+
+@[extern "sin"] constant Float.sin : Float → Float := arbitrary _
+@[extern "cos"] constant Float.cos : Float → Float := arbitrary _
+@[extern "tan"] constant Float.tan : Float → Float := arbitrary _
+@[extern "asin"] constant Float.asin : Float → Float := arbitrary _
+@[extern "acos"] constant Float.acos : Float → Float := arbitrary _
+@[extern "atan"] constant Float.atan : Float → Float := arbitrary _
+@[extern "atan2"] constant Float.atan2 : Float → Float → Float := arbitrary _
+@[extern "sinh"] constant Float.sinh : Float → Float := arbitrary _
+@[extern "cosh"] constant Float.cosh : Float → Float := arbitrary _
+@[extern "tanh"] constant Float.tanh : Float → Float := arbitrary _
+@[extern "asinh"] constant Float.asinh : Float → Float := arbitrary _
+@[extern "acosh"] constant Float.acosh : Float → Float := arbitrary _
+@[extern "atanh"] constant Float.atanh : Float → Float := arbitrary _
+@[extern "exp"] constant Float.exp : Float → Float := arbitrary _
+@[extern "exp2"] constant Float.exp2 : Float → Float := arbitrary _
+@[extern "log"] constant Float.log : Float → Float := arbitrary _
+@[extern "log2"] constant Float.log2 : Float → Float := arbitrary _
+@[extern "log10"] constant Float.log10 : Float → Float := arbitrary _
+@[extern "pow"] constant Float.pow : Float → Float → Float := arbitrary _
+@[extern "sqrt"] constant Float.sqrt : Float → Float := arbitrary _
+@[extern "cbrt"] constant Float.cbrt : Float → Float := arbitrary _
+
+instance : HasPow Float Float := ⟨Float.pow⟩
diff --git a/tests/lean/run/float1.lean b/tests/lean/run/float1.lean
new file mode 100644
index 0000000000..061a49866b
--- /dev/null
+++ b/tests/lean/run/float1.lean
@@ -0,0 +1,8 @@
+def main : IO Unit := do
+IO.println ((2 : Float).sin);
+IO.println ((2 : Float).cos);
+IO.println ((2 : Float).sqrt);
+IO.println ((2 : Float) ^ (200 : Float));
+pure ()
+
+#eval main