Zulip Chat Archive

Stream: maths

Topic: Isabelle

view this post on Zulip Sebastien Gouezel (Aug 27 2018 at 07:00):

I just wanted to thank @Johannes Hölzl for this in Isabelle:

have "81 * exp(8 * ln 2/21) / 4 ≤ 80/3"
 by (approximation 8)

(where 80/3 is just some good upper approximation I chose for simplicity, accurate within 1%)

view this post on Zulip Johannes Hölzl (Aug 27 2018 at 09:47):

Thanks! How long did it take to figure out 8? And how long did you play around to find the expression which finally worked :-)

view this post on Zulip Sebastien Gouezel (Aug 27 2018 at 10:01):

To chose a good upper approximation, I computed the continued fraction expansion of 81 * exp(8 * ln 2/21) / 4 and truncated it to some terms. To figure out the 8, I tried first with 5 but it failed, then 6, then 7, then 8, and it succeeded. Simple enough :) For another numerical approximation in the same file, I had to go up to approximation 17 (which I found by dichotomoy), but the proof is still almost instantaneous. That's a wonderful tool! (If I had to give a proof by hand, it would be super-tedious and certainly 100 lines long...)

Last updated: May 12 2021 at 08:14 UTC