This is a pretty interesting thread, though not the best advertisement for Coq: https://twitter.com/andrejbauer/status/1269367589936955394
What's the most confusing thing for a mathematician when they start using a proof assistant, speaking from your personal experience? (Computer scientists, plese do not answer this one.)
Last updated: Dec 07 2023 at 04:02 UTC