Conferences

[dmm]

The details will be in comments (I have mixed feeling about all this).

I am seeing people talking about their talks being accepted for Strange Loop. It seems that this will be the last Strange Loop conference (I have no idea why).

Terence Tao is co-organizing "AI to Assist Mathematical Reasoning" online workshop (June 12-14).

Joint conference of "Algebra and Coalgebra in Computer Science" and "Mathematical Foundations of Programming Semantics" is on June 19-23 (free for those who participate online).

Comments

[dmm]

This is a part of what people are doing.

It's a large field now, people are trying a variety of things. Auto-formalization is a big one, for obvious reasons (e.g. https://arxiv.org/abs/2205.12615)

Then there is a dichotomy between working in theorem provers and generating readable proofs (Tim Gowers has been returning to his 10-year-old exploration https://arxiv.org/abs/1309.4501 recently, and I believe his intent has been to create a more anthropomorphic system, which would be closer to inner workings of (some) human mathematicians).

But, yes, for example, https://arxiv.org/search/?searchtype=author&query=Szegedy%2C+C has a number of papers on this between 2016 and 2023, https://arxiv.org/search/cs?searchtype=author&query=Urban%2C+J has a number of papers on this between 2010 and 2023, etc, etc. A large field, different things are going on...

[chaource]

This is great. At some point, those developments could be used to make an intelligent compiler that can (at least sometimes) perform undecidable tasks. For example, type checking in many lambda calculi is undecidable; generating code from type in a dependently-typed language is undecidable; etc.