This is a soft question aimed at understanding whether there is any value to publishing formally verified libraries. I have formally verified (in Coq) implementations of:

  1. synthetic differential geometry
  2. Chains of recurrences

Are these of interest in terms of publication anywhere? what is the bar for "what can be formally verified and published"? Are these even "put on on Arxiv" worthy? In general, what's the boundary that separates "routine proof" from "publishable proof"?

Thanks a lot!

  • 1
    $\begingroup$ Places like CPP (certified proofs and programs) are certainly interested in experience reports for formalizing mathematics. Looking at the program from this last year many of the submissions were about this (popl20.sigplan.org/home/CPP-2020#event-overview). I do not think that the sdg formalization you put is quite at the stage to be submitted though, since it is doesn't really contain any theorems, just statements of axioms. $\endgroup$ – Daniel Gratzer Feb 12 '20 at 15:33
  • $\begingroup$ Thanks! I'd be interested in a spectrum of conferences: CPP looks far too demanding in terms of the scale of the proofs I'm interested in formalizing. $\endgroup$ – Siddharth Bhat Feb 12 '20 at 15:42
  • $\begingroup$ Regarding synthetic differential geometry: I agree. That went on hiatus after I found out that building models for SDG is quite hard --- I was wondering if it was a good fit for CPP $\endgroup$ – Siddharth Bhat Feb 12 '20 at 15:42
  • 1
    $\begingroup$ There are several, see e.g. here. $\endgroup$ – Martin Berger Feb 12 '20 at 18:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.