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/
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
