What is the future of #math #AI and #formalization ? Will AI just replace the work of mathematicians? Or will it rather be a complement? I imagine a complementary role and so I'm still optimistic, however, this might be naive, and it's good to ponder alternatives. (1/2)

🚨New paper alert!🚨 My new paper with Qi Zhu is out! We show that condensed mathematics, due to Scholze & Clausen, admits a fractured structure. This means condensed objects are "gros objects" with the "petit objects" given by regular sheaves on spaces! Links in next post👇

🎓 PhD Position Alert! 🚀 Are you looking for a PhD position in category theory and type theory? 📚✨ Then check out this exciting opportunity at Utrecht University 🇳🇱 under the supervision of Paige Randall North! 🗓 Deadline: April 6th, 2026 🔗 Link in the next post 👇

🚨 Putting this back on your radar: The deadline for the ICERM Graduate Training Workshop on ∞-categories with proof-assistants (organized with @emilyriehl.bsky.social and Jonathan Weinberger) is getting close! 📬Application deadline: March 31, 2026. Full details + links in the post below 👇

2025 was an exciting year!🥳🥳🥳 2026 will be an even better year!🎉🎉🎉 If you want to know more about what I have been up to this year, and what my plans are for 2026, check out the next post👉

Looking for a post-doctoral position in algebraic topology? Check out this position in the group of homotopykat.bsky.social at EPFL! If you have any questions about the position, the group, EPFL or living in @villelausanne.bsky.social, then please reach out! Links and more details below👉

🌞Summer School Announcement🌞 🎓∞-Category Theory at ICERM!🎓 I am happy to announce that together with @emilyriehl.bsky.social and Jonathan Weinberger we are organizing a Graduate Training Workshop teaching ∞-category theory via proof assistants!🧠💻 More infos in the next post👉

This past year I spent some time thinking about filter quotient models of homotopy type theory. I am happy to announce that I now have a chance to talk about it 📍 First Meeting of the Higher Structures Network, Nottingham, UK 🗓️ Thursday Nov. 19 Links in the next post👉

🚨 Position alert 🚨 Looking for a position that involves programming, quantum computing, and cutting edge mathematics? Then check out this Research Software Engineer position in the research group of Cihan Okay: www.mathjobs.org/jobs/list/27...

🚀 Exciting news! I’m organizing the conference Formalizing Higher Categories at Institut Mittag-Leffler (Stockholm, June 2026) — bringing together experts to explore how far ∞-category theory can be formalized in proof assistants (like Lean). More info in the next post 👇

Every postdoc whenever fall comes around again: #AcademicLife #JobMarket #PostDocLife

Definitiv ein guter Schritt von ‪@bettinamartin.bsky.social für unser Land #MV und @unigreifswald.bsky.social um Talente aus den #USA anzuziehen! -Natürlich nur wenn Interessierte auch passend unterstützt und/oder finanziert werden können- www.ostsee-zeitung.de/mecklenburg-...

This article by the always insightful @emilyriehl.bsky.social is very relatable indeed: www.scientificamerican.com/article/math... #AI doing exercises and problems in mathematics looks impressive, but how does that relate to research mathematics? The honest answer is: we don't know yet!

Rare #achievement unlocked: Having 3 consecutively numbered papers on the #arXiv! Never seen this before, so I count this as a record! If you know of any other cases like this (or even higher) let me know!

🚨 New paper(s) alert! 🚨 In a series of 3 papers I use a technical construction (filter quotients) to contruct models of (simplicial) homotopy type theory (HoTT). This helps better understand #formalization and possibly the role for #AI in (simplicial) HoTT. Links in the next posts:

Nima Rasekh Simplicial Homotopy Type Theory is not just Simplicial: What are $\infty$-Categories? https://arxiv.org/abs/2508.07737

Nima Rasekh Non-Standard Models of Homotopy Type Theory https://arxiv.org/abs/2508.07736

Nima Rasekh Filter Quotient Model Structures https://arxiv.org/abs/2508.07735

I am very excited to announce that my joint paper with @homotopykat.bsky.social titled ``Shadows are Bicategorical Traces" has been accepted in Advances in Mathematics. The text might be very technical, but the intro is meant to be somewhat accessible to the casual reader: arxiv.org/abs/2109.02144

Taichi Uemura Colimits in the $\infty$-category of $\infty$-topoi and \'etale morphisms https://arxiv.org/abs/2506.10431

I recently contributed to the FrontierMath Tier 4 Challenge from @epochai.bsky.social which aims to design an #AI benchmark for advanced mathematics: epoch.ai/frontiermath... I found this experience fascinating & so elaborated on it somewhat. Check it out: www.linkedin.com/posts/nimara...

Verrückte Zeiten wenn ich & #MarkusSoeder die selbe Meinung haben (wenn auch ein Exil-‪@harvard.edu‬ ein bisschen ulkig ist). Internationale Wissenschaft nach 🇩🇪 zu holen ist genau der richtige Ansatz und muss finanziell unterstützt werden! www.spiegel.de/politik/deut... via @derspiegel @spiegel.de

A first concrete step by @ec.europa.eu seizing the current situation and further investing in the scientific future of 🇪🇺 via the (aptly named) "Choose Europe" Initiative. Looking forward to further targeted efforts attracting global scientific talent! commission.europa.eu/topics/resea...

Science and research in 🇪🇺 is currently in a unique moment. If there is an effort to seize the moment and attract scientific talent. Similarly, there is a chance for a strong role for the Euro as a real reserve currency that can compete with💲, with proper regulatory choices.

Couldn't have said it better myself! 🇪🇺 should indeed act more confidently and shape science and the technology of the future. Für 🇩🇪 gilt das besonders! From @pkrugman.bsky.social "Letter to Europe": paulkrugman.substack.com/p/a-letter-t...

It's hard to exaggerate what a 72% cut in NSF funding will mean for mathematics in the US and the world. Ideally the rest of the world (maybe EU?) will step up, but for the moment this is truly a disappointing development www.nytimes.com/interactive/...

A rare occasion where I put a paper on the arXiv after being accepted (in Homology, Homotopy and Application). In this short paper I show that we can nicely comine Lurie's unstraightening for quasi-categories with the more general ∞-cosmos framework of @emilyriehl.bsky.social and Verity.

You are an early career mathematician looking for postdoc positions (or you know somebody)? Then check out this postdoc positions at the MPIM in Bonn with deadline 24.05: www.mpim-bonn.mpg.de/application Please share with whoever might be interested. If you have questions feel free to ask!

This is an exciting development! Congrats @emilyriehl.bsky.social ! Hope this encourages further editorial boards to leverage their collective ability to shape research and its accessibility!

Check out my talk "Formalization: Proving Theorems via Computers" organized by #Zaiku starting today (Monday) at 17 GMT: youtube.com/live/vNVXPI8... #formalization

I'm very excited about my upcoming talk about the role of #formalization and #AI in the future of mathematics, that is being organized by the Zaiku Group! It is Monday 17.03 at 17 GMT and is streamed online. If you want to attend, you can sign up here: quantumformalism.academy/proving-theo...

Rare msg in 🇩🇪: Es wird derzeit viel von der Zeitenwende und Umbruch in der Politik geredet. Das bedarf konkrete Fortschritte in der Wissenschaft in 🇩🇪. Hier die 10 interessanten Vorschläge der Max-Planck-Gesellschaft mit sehr vielen guten Ideen: www.mpg.de/24266790/fue...

On Thursday (13.3) I am giving a talk in Lean­ing In! 2025 <https://leaning.in/> in Berlin on formalizing ∞-categories. There are options to attend remotely: jessealama.gumroad.com/l/leaning-in... If that doesn't work, here is already a sneak peek of my talk: www.linkedin.com/posts/nimara...

(1/7) I've been thinking about the future of computers in mathematics. What role might they play in ten or fifteen years? How will recent advancements in AI and formalization shape their impact?

This Friday (7.2) I'm giving a talk in the DutchCats Seminar at Radboud Universiteit Nijmegen titled "From Mathematical Foundations to (Higher) Categories" I want to convince a foundations-minded audience that ∞-categories are interesting, due to their dependence on foundations dutchcats.github.io

I am happy to announce that my paper joint with Niels van der Weide, Benedikt Ahrens & Paige Randall North has been published at Computer Science Logic 2025. We show how univalent mathematics can be used to study intricate (higher) categories & formalize it in Coq UniMath doi.org/10.4230/LIPI...

This Thursday (30.1) I'm giving a talk in TopICS at VU titled "From Internal Higher Categories to the Foundation of Mathematics" I want to explain how basic questions in ∞-category theory relate to mathematical foundations (in a way I found surprising) guyboyde.wordpress.com/topics-sched...

The Yoneda embedding is arguably the most important functor in category theory, yet incredibly hard and technical to generalize to ∞-categories. Luckily Ulrik Buchholtz, Danniel Gratzer & Jonathan Weinberger found a new approach relying on a more fitting foundation: sHoTT! arxiv.org/abs/2501.13229

David Reutter, Markus Zetto Enriched $\infty$-categories as marked module categories https://arxiv.org/abs/2501.07697

Lean Together 2025 is happening (online conference: details leanprover-community.github.io/lt2025/). I've put the videos for day 1 of the conference up on YouTube: www.youtube.com/watch?v=ZPPD...

I introduced formalization and the value of computers in proofs to a math audience in the math departments Christmas colloquium at @unigreifswald.bsky.social very much motivated by @xenaproject.bsky.social 2022 Plücker Lecture at Uni Bonn Check out the slides: nimarasekh.github.io/Christmas_Gr...

Lyne Moser, Joost Nuiten Modeling $(\infty,1)$-categories with Segal spaces https://arxiv.org/abs/2412.10359

(1/5) I have recently started contributing to the ∞-Cosmos Project (emilyriehl.github.io/infinity-cos...), commenced by Emily Riehl, with the help of the very patient Matej Penciak (github.com/mpenciak)!

I recently had the pleasure of being interviewed by my former Master student, Qi Zhu. It was quite a lot of fun and includes some math, but also many other topics. Here is the transcript, in case you got couple minutes for a fun read: journeysofmathematicians.wordpress.com/2024/11/01/n...

My latest talk in the Second Virtual Workshop on Double Categories (bryceclarke.github.io/virtual-doub...), about double categories and univalent mathematics, is now online: www.youtube.com/watch?v=mAjE...

Happy to announce my newest paper, which studies how univalent foundations gives us a more refined understanding of category theory. We apply this new approach to double categories, which have found a variety of applications and, due to their intricate nature, significantly benefit from our method.

There has been a recent effort to "internalize" higher categories, which generalizes known results significantly and has found many applications in geometry and logic. A recent paper ( arxiv.org/abs/2402.01396 ) in particular focuses on its (oo,2)-categorical and oo-cosmos theortical aspects!

Dependent type theory is the cornerstone of modern theoretical computer science, a key aspect of which are constructors such as Σ- Π-types. Recent work ( arxiv.org/abs/2402.00331 ) shows how these types manifest in many areas of math: (1) set theory (2) category theory (3) topology (4) geometry

While this recent paper ( arxiv.org/abs/2401.17848 ) is titled "Unstable p-completion in motivic homotopy theory", it also does an interesting job studying new aspects of higher topos theory, which is the appropriate abstract setting for derived geometry.

Double categories are becoming more important by the day! Latest example is the introduction of premonoidal double categories and the the study of Kleisli double categories by Femić: arxiv.org/abs/2401.17494