Clarification of Skepticism

Timothy Y. Chow tchow at
Fri Mar 5 17:57:21 EST 2021

Freek Wiedijk wrote:

> I agree with Harvey that you really would like a system in which 
> experimenting with data, graphing and making diagrams, _and_ 
> representing the definitions, statements and proofs is all together. 
> Currently we have systems like Mathematica on the one hand, and the 
> proof assistants on the other hand, and they are not close to merging 
> yet. (I once had a project to work towards this goal -- it was called 
> FEAR, formalising elementary analysis rigorously -- but that 
> unfortunately never went beyond a prototype stage.)

Another prototype worth mentioning was created by Muhammad Taimoor Khan 
for his 2014 doctoral dissertation, "Formal specification and verification 
of computer algebra software":


More information about the FOM mailing list