Proof assistants and formalised mathematics in the MSC database

Question

I was looking at the MSC2020 database and I find it hard to identify a field suitable for works about proof assistants and formalised mathematics. 03B70 ("Logic in Computer Science") might be the closest one, but it does not look optimal to me. My questions are

1. Do you think a better subject class exists?
2. If we end up agreeing that there is none (and that one might be needed), is there a way to propose this to the AMS?

Answer 1

TL;DR: Based on the descriptions in the MSC2020 alone, I would use the new section 68Vxx, specifically the subject classification 68V20 (or maybe 68V15) if one is formalizing mathematics in a proof assistant. (However, 68 is CS, so if one is concerned that their work be recognized as pure mathematics, then maybe it shouldn't be the primary classification of the work.)

---

There appears to be a new section in the 2020 MSC Subject Classification:

• 68Vxx Computer science support for mathematical research and practice
  • 68V05 Computer assisted proofs of proofs-by exhaustion type {For rigorous numerics, see 65Gxx; for proofs employing automated or interactive theorem provers, see 68V15}
  • 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) [See also 03B35]
  • 68V20 Formalization of mathematics in connection with theorem provers [See also 03B35, 68V15]
  • 68V25 Presentation and content markup for mathematics
  • 68V30 Mathematical knowledge management
  • 68V35 Digital mathematics libraries and repositories
  • 68V99 None of the above, but in this section

Note some of the above subject classifications also cross reference 03B35, but this classification (from 2010) seems quite vague:

• 03B35 Mechanization of proofs and logical operations [See also 68V15]

Even, 03B70, the subject classification you mentioned (which seems to be the de facto standard in the small, biased selection of arXiv papers I've looked at) also cross references 68-XX:

• 03B70 Logic in computer science [See also 68-XX]

Last, the computer science section 68-XX also mentions the availability of the classifications -04 for "papers containing software, source code, etc. in a specific mathematical area", e.g.

• 14-04 Software, source code, etc. for problems pertaining to algebraic geometry

---

There is a small discussion on the Lean Zulip about this new section.

---

Here are papers on arXiv using 68V20 and 68V15.

---

I'd also love to get an answer from someone involved in the creation of 68Vxx or from anyone who feels that 68Vxx doesn't work for them.