MSC

Stream: general

[Johan Commelin]

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]

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

[Patrick Massot]

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]

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

[Matthew Ballard]

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]

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

:oops:

[Adam Topaz]

Looks like foo-04 is a catch-all

[Matthew Ballard]

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

[Adam Topaz]

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

[Angeliki Koutsoukou Argyraki]

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]

This came up on the new Proof Assistant StackExchange.