English
There exists a rational r = 363916618873/133877442384 with |exp(1) - r| ≤ 10^-20.
Русский
Существует рациональное число r = 363916618873/133877442384 такое, что |exp(1) - r| ≤ 10^-20.
LaTeX
$$$|\exp(1) - \frac{363916618873}{133877442384}| \le 10^{-20}$$$
Lean4
theorem exp_one_near_20 : |exp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20 :=
by
apply exp_approx_start
iterate 21 refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
refine exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) ?_
norm_num1