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 <kirby.ur...@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. > >
_______________________________________________ Edu-sig mailing list Edu-sig@python.org https://mail.python.org/mailman/listinfo/edu-sig
