infinity cosmos project at the "AI for Mathematics" workshop

Stream: Infinity-Cosmos

[Emily Riehl]

I'll be in Berkeley this coming week with some other Lean folks at a joint Simons Institute / SL Math workshop. Is anyone else going to be around?

[Emily Riehl]

I ask because I'd like to try to tackle one of the tasks on our new tasks list --- collaboratively if anyone is interested and on my own otherwise. So if there's something on the list you were hoping to work on yourself, now's the time to claim it. Alternatively, if you'll be in Berkeley, get in touch!

[Julian Komaromy]

Are there any preferences as to what newcomers should try to work on first? I was thinking of claiming 2-truncated quasi-categories and working on that in the next week, but I wouldn't want to take it away from someone with more experience if there is interest in getting it done quickly.

[Emily Riehl]

Welcome! I'm generally happy to give newcomers first dibs. Please get in touch if you need help or want feedback, particularly with @Nick Ward who has experience developing infrastructure for truncated simplicial sets.

[Nick Ward]

Happy to answer any questions @Julian Komaromy. The truncated simplicial set infrastructure in question was just recently merged (#20668), so it would be helpful to know about anything that is unclear (or broken).