# Zulip Chat Archive

## Stream: general

### Topic: MSC

#### Johan Commelin (Jul 30 2021 at 17:23):

I just learned from @Angeliki Koutsoukou Argyraki

It is worth reminding that for the first time, formalised mathematics using proof assistants appeared as a class in the 2020 Mathematics Subject Classification (Class 68XXX with several subclasses) in January 2020

#### Patrick Massot (Jul 30 2021 at 17:24):

I wonder who those people told about it since they haven't told us...

#### Patrick Massot (Jul 30 2021 at 17:26):

More precisely it seems to be in 68VXX. Knowing that 68XXX means "computer science", there is still quite a bit of work to convince people we're doing mathematics..

#### Patrick Massot (Jul 30 2021 at 17:27):

There is also 03B35 in "general logic" :rolling_eyes:

#### Matthew Ballard (Jul 30 2021 at 17:30):

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

for convenience.

#### Adam Topaz (Jul 30 2021 at 17:31):

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

:oops:

#### Adam Topaz (Jul 30 2021 at 17:31):

Looks like foo-04 is a catch-all

#### Matthew Ballard (Jul 30 2021 at 17:32):

~~Are there emoji in the classification documentation now?~~ There should be emoji in the documentation.

#### Adam Topaz (Jul 30 2021 at 17:32):

Alghough 14F04 doesn't exist, while 14FXX does.

#### Angeliki Koutsoukou Argyraki (Jul 30 2021 at 17:55):

Yes, sorry for the typo, I should have written 68VXX instead of 68XXX. And, yes, the general class is labeled as "Computer Science" indeed, but keep in mind, IT IS within the Mathematics Subject Classification now after all, meaning IT IS recognised as mathematics :smile: It is a big thing! See: https://mathscinet.ams.org/msnhtml/msc2020.pdf Btw, I first found out from an email by Michael Kohlhase to the CICM mailing list on 18/2/2020

#### Jason Rute (Mar 17 2022 at 12:36):

This came up on the new Proof Assistant StackExchange.

Last updated: Dec 20 2023 at 11:08 UTC