English
π is less than 3.14159265358979323847.
Русский
π меньше 3.14159265358979323847.
LaTeX
$$$\\pi < 3.14159265358979323847$$$
Lean4
theorem pi_lt_d20 : π < 3.14159265358979323847 := by
-- bound[314159265358979323847*^-20, Iters -> 34, Rounding -> .5, Precision -> 46]
pi_upper_bound [215157040700 / 152139002499, 936715022285 / 506946517009, 1760670193473 / 897581880893,
2 - 6049918861 / 628200981455, 2 - 8543385003 / 3546315642356, 2 - 2687504973 / 4461606579043,
2 - 1443277808 / 9583752057175, 2 - 546886849 / 14525765179168, 2 - 650597193 / 69121426717657,
2 - 199969519 / 84981432264454, 2 - 226282901 / 384655467333100, 2 - 60729699 / 412934601558121,
2 - 25101251 / 682708800188252, 2 - 7156464 / 778571703825145, 2 - 7524725 / 3274543383827551,
2 - 4663362 / 8117442793616861, 2 - 1913009 / 13319781840326041, 2 - 115805 / 3225279830894912,
2 - 708749 / 78957345705688293, 2 - 131255 / 58489233342660393, 2 - 101921 / 181670219085488669,
2 - 44784 / 319302953916238627, 2 - 82141 / 2342610212364552264, 2 - 4609 / 525783249231842696,
2 - 4567 / 2083967975041722089, 2 - 2273 / 4148770928197796067, 2 - 563 / 4110440884426500846,
2 - 784 / 22895812812720260289, 2 - 1717 / 200571992854289218531, 2 - 368 / 171952226838388893139,
2 - 149 / 278487845640434185590, 2 - 207 / 1547570041545500037992, 2 - 20 / 598094702046570062987,
2 - 7 / 837332582865198088180]
