Re: adventures in using Python as a calculator

Speaking of proofs and not calculators, this dropped on HN this week:

"Formalizing 100 theorems in Coq"
> This is an appendix to Freek Wiedijk's webpage on the "top 100"
mathematical theorems, to keep track of the statements of the theorems that
are formalised in Coq.
https://madiot.fr/coq100/

... There's a JS implementation of Coq:
https://github.com/ejgallego/jscoq/blob/master/README.md#homotopy-type-theory

https://github.com/HoTT/book

Optimal Coq/Jupyter integration may require extending the kernel interface:
https://github.com/jupyter/jupyter/issues/333

Is there a good way to do proof modeling in Python?

What's your favorite Python-basee CAS?

On Sunday, October 7, 2018, kirby urner <[email protected]> wrote:

>
> A stereotype some people have, of computers, is they're like giant
> calculators on steroids.
>
> Then they find as much "text processing" goes on as "number crunching" -- ala
> "regular expressions" -- and forget about the calculator model.
> Calculators don't do strings, let alone much in the way of data files.
> Of course that line got blurred in the golden age of programmable
> calculators (HP65 etc.).
>
> However, the Python docs start with Using Python as a Calculator in
> Guido's tutorial.
>
> Perhaps we could do more to fulfill the "on steroids" expectations (that
> the computer is a "beefed up" calculator device) by exploring our number
> types in more depth, and in particular by exploiting their superhuman
> abilities in the extended precision department.
>
> Yes, the int type is awesome, now that it integrates long int (for those
> new to Python, these used to be separate), but lets not forget Decimal and
> also... gmpy, or actually gmpy2.
>
> I've probably lost even some seasoned Python teachers in jumping to that
> relatively obscure third party tool, providing extended precision
> numeracy beyond what Decimal (in Standard Library) will do.  gmpy has a
> long history, predating Python.  I'm not the expert in the room.
>
> In particular, it does trig.
>
> Our Python User Group used to get one of the package maintainers from
> nearby Mentor Graphics (Wilsonville). He was adding complex numbers to the
> gmpy mix, and was in touch with Alex Martelli.  I enjoyed our little
> chats.
>
> Without having all the higher level math it might take to actually prove
> some identity, and while starting to learn of those identities nonetheless,
> extended precision would seem especially relevant.
>
> "Seriously, I can generate Pi with that summation series?" Lets check.
>
> Just writing the program is a great workout.
>
> Some subscribers may recall a contest here on edu-sig, for Pi Day (3/14),
> to generate same to a 1001 places, given one of Ramanujan's convergence
> expressions for the algorithm.
>
> https://github.com/4dsolutions/Python5/blob/master/Pi%20Day%20Fun.ipynb
> http://mathforum.org/kb/thread.jspa?threadID=2246748
>
> I had an adventure in gmpy2 just recently when my friend David Koski
> shared the following:
>
>     from math import atan as arctan
>     Ø = (1 + rt2(5))/2
>     arctan( Ø ** 1) -  arctan( Ø ** -1) == arctan(1/2)
>     arctan( Ø **-1) -  arctan( Ø ** -3) == arctan(1/3)
>     arctan( Ø **-3) -  arctan( Ø ** -5) == arctan(1/7)
>     arctan( Ø **-5) -  arctan( Ø ** -7) == arctan(1/18)
>     arctan( Ø **-7) -  arctan( Ø ** -9) == arctan(1/47)
>     arctan( Ø **-9) -  arctan( Ø **-11) == arctan(1/123)
>     ...
>
> Without offering any kind of algebraic proof, I just wanted to see if the
> arithmetic panned out.
>
> These denominators on the right turned out to be a "bisection of the Lucas
> numbers" (like Fibonaccis with a different seed).  That's a great job for
> a Python generator, and only integers are involved.
>
> But am I really confined to verification (not proof) using floating
> points?  Not at all.  At first it seemed that way thought, because whereas
> Decimal supports powering and roots, it's not equipped with atan.
>
> Then I remembered gmpy2 and could all of a sudden push the number of
> verifying decimals out past 92.  Definitely a calculator couldn't do this.
>
> https://github.com/4dsolutions/Python5/blob/master/VerifyArctan.ipynb
>
> Math students the world over, if free of the tyranny of calculators -- or
> at least allowed to aid and abet (supplement) with Raspberry Pi etc. -- get
> to dabble in these industrial strength algorithms, a part of their
> inheritance.
>
> Indeed lets use Python as a calculator sometimes, in accordance with said
> Python.org tutorial.
>
> A much stronger calculator, with a bigger screen, more keys, and a lot
> more horsepower.
>
> Kirby
> PS:  I ran into this problem with gmpy2.atan: the above convergence wasn't
> verifying beyond like 19 digits.  When I switched to gmpy2.atan2 istead,
> everything started to work out.  The question being, why should atan(x) vs
> atan2(y,x) differ except in terms of API?  gmpy2.atan2(y,x) computes the
> arctan of y/x but in some other way apparently.  Food for thought.  I did
> do some digging in the docs.
>
>

_______________________________________________
Edu-sig mailing list
[email protected]
https://mail.python.org/mailman/listinfo/edu-sig