[FOM] Improving Set Theory/Self Proving

[Lawrence Paulson]

It is simply that there is an immense difference in what they do. For LaTeX you are simply putting marks on a page, and when you write D^2 you aren’t concerned with the numerous different meanings that could have. For computer algebra, you are concerned with a tiny fragment of the world of mathematics. But with proof assistants, people want to talk about anything from block designs to forcing to homology theory and expect it all to work smoothly.

Larry Paulson
On 14 Jan 2020, 23:18 +0000, Timothy Y. Chow <tchow at math.princeton.edu>, wrote:
>
> On the other hand, I am interested in what obstacles are preventing proof
> assistants from becoming as widely adopted as, say, computer algebra
> systems or even LaTeX.
>
> In short, there still seems to be room for fresh design ideas. Of course
> there remains the problem that ideas are cheap, while writing a kernel and
> building libraries and creating documentation and building a user base are
> expensive.
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200115/d7ee5d01/attachment-0001.html>