22
$\begingroup$

I am interested in contributing to the formalization of mathematics, but I don't know the extent to which such activities are publishable. Here are some questions in this vein:

  1. How can one determine whether a piece of formalized mathematics is publishable? If the math is new, then it's publishable even without formalization. If the math is old, but the formalization is new, then I assume it is publishable. What if a piece of mathematics has already been formalized in language X, but you are the first to formalize it in language Y?

  2. What are the appropriate venues to publish formalized mathematics? I assume there is a hierarchy of outlets, but I'm not familiar with them.

  3. What are the best practices for publishing formalized mathematics that make use of libraries that change over time? For example, if one writes a proof in Lean, must the contribution be included in mathlib before submitting for publication somewhere?

$\endgroup$
1
  • 4
    $\begingroup$ Re 3: One great reason to incorporate a proof into Lean's mathlib or similar is to ensure that it keeps being maintained. Sadly, a lot of original formal proofs have fallen to bit rot and are no longer of much use. Incidentally, that also explains why publishing formal proofs is somewhat difficult. $\endgroup$ Mar 4, 2022 at 2:52

3 Answers 3

11
$\begingroup$

The ITP and CPP conferences regularly accept papers on mechanised mathematics. See previous programs at, for example:

  • ITP 2016, where there were among others, papers such as A Formal Proof of Cauchy’s Residue Theorem and On the Formalization of Fourier Transform in Higher-order Logic
  • CPP 2021, where there was Formalizing Category Theory in Agda.
$\endgroup$
6
$\begingroup$
  1. I don't know if there are well-established rules yet. My guess would be that it depends on how significant the differences are between X and Y.

  2. If the mathematics is new, then of course it can be published anywhere that that mathematics could be published, with the formalization as a bonus. If only the formalization is new, some CS conferences have been mentioned already, and I would expect some CS journals would also accept at least some papers of this sort. Also I don't know anything about it, but I have heard there is a Journal of Formalized Reasoning (although at present their web site doesn't seem to be responding).

  3. As François said in a comment, inclusion in a library is valuable to guard against bitrot. However, it can also be useful to mark the exact release of a library that the formalization either imports or is included in, since future changes to the library can either break the formalization (if it isn't included) or include changes to or reorganization of the formalization that may break some of the references from the paper.

$\endgroup$
5
$\begingroup$

I once asked a similar question in the Coq Zulip chat (regular link, no-login-needed link). This was my takeaway:

  1. If your formalization is interesting as code, you can publish it from that angle. In particular:

Karl Palmskog: I've only been in the CPP PC once, but what we look for are descriptions of how the formalization was done, i.e., the encoding of logics, properties, etc. Also what kind of automation was used, how much effort did it take, is it reusable, can it be connected to other libraries, how were the results validated. If there is some interesting theoretical or practical application of a formally proved theorem that has been successfully done, this is a form of validation.

I also get the impression you could have an easy time publishing formalizations of well-known and previously-unformalized mathematical results, particularly if you found mistakes in the known paper "proofs".

For formalizations that don't fit either of the previous two cases, I think they would still be publishable, but perhaps in smaller venues, and I would like to hear from anyone with experience here.

  1. Some relevant venues:
  • Certified Programs and Proofs, CPP
  • Interactive Theorem Proving, ITP
  • Journal of Automated Reasoning, JAR
  • Some FLOC Workshops
  1. Place your code somewhere like Zenodo. Furthermore, try to include it in a well-maintained library. If you manage to include it in your proof assistant's standard library, great! But there are often other good libraries available, possibly with a better subject-matter fit.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.