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-theor... 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 <kirby.urner@gmail.com> 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.