iiinova — where your digital self keeps evolving

Nima Rasekh @nimarasekh.bsky.social · 14/06/2026

✨ Conference wrap-up! ✨ This week we gathered at the Mittag-Leffler Institute for Formalizing Higher Categories — a wonderful week of math, formalization, proof assistants, and collaboration. 🧠💻🚀 #HigherCategories #Formalization #ProofAssistants #AIForMath #CategoryTheory (1/3)

Nima Rasekh @nimarasekh.bsky.social · 07/06/2026

In June 2024, during the “Prospects of Formal Mathematics” trimester in Bonn, a coffee-room chat with Johan Commelin ☕️ turned into an idea: formalizing higher categorical concepts is hard, so there really should be a conference about it! 🚀 More details below 👇 #FormalMathematics (1/2)

Nima Rasekh @nimarasekh.bsky.social · 23/03/2026

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)

100

Nima Rasekh @nimarasekh.bsky.social · 11/03/2026

🚨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👇

151

Nima Rasekh @nimarasekh.bsky.social · 07/03/2026

🎓 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 👇

111

Nima Rasekh @nimarasekh.bsky.social · 27/02/2026

🚨 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 👇

031

Nima Rasekh @nimarasekh.bsky.social · 30/12/2025

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👉

100

Nima Rasekh @nimarasekh.bsky.social · 07/11/2025

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👉

homotopykat.bsky.social

Kathryn Hess Bellwald (@homotopykat.bsky.social)

Mathematician, lover of mountains, mother of four, EPFL professor

Nima Rasekh @nimarasekh.bsky.social · 07/11/2025

🌞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👉

183

Nima Rasekh @nimarasekh.bsky.social · 31/10/2025

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👉

120

Nima Rasekh @nimarasekh.bsky.social · 12/10/2025

🚨 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...

mathjobs.org

MathJobs from the the American Mathematical Society

Mathjobs is an automated job application system sponsored by the AMS.

Nima Rasekh @nimarasekh.bsky.social · 25/09/2025

🚀 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 👇

100

Nima Rasekh @nimarasekh.bsky.social · 19/08/2025

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!

scientificamerican.com

AI Crushed the Math Olympiad—Or Did It?

AI models supposedly did well on International Math Olympiad problems, but how they got their answers reminds us why we still need people doing math

011

Nima Rasekh @nimarasekh.bsky.social · 14/08/2025

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!

Nima Rasekh @nimarasekh.bsky.social · 12/08/2025

🚨 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:

122

Reposted by Nima Rasekh

arxiv math.CT @arxiv-math-ct.bsky.social · 12/08/2025

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

arxiv math.CT @arxiv-math-ct.bsky.social · 12/08/2025

Reposted by Nima Rasekh

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

arxiv math.CT @arxiv-math-ct.bsky.social · 12/08/2025

Reposted by Nima Rasekh

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

Nima Rasekh @nimarasekh.bsky.social · 27/06/2025

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

lnkd.in

This link will take you to a page that’s not on LinkedIn

arxiv math.CT @arxiv-math-ct.bsky.social · 13/06/2025

Reposted by Nima Rasekh

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

Nima Rasekh @nimarasekh.bsky.social · 07/06/2025

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...

000

Nima Rasekh @nimarasekh.bsky.social · 06/06/2025

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

spiegel.de

Ministerin Bär plant »Rundum-sorglos-Paket« für ausländische Forschende

US-Präsident Trump macht ihnen das Forschen schwer, Wissenschaftsministerin Bär will nun Spitzenkräfte von US-Hochschulen nach Deutschland holen. Parteifreund Söder schwärmt bereits von einem »Exilcam...

011

Nima Rasekh @nimarasekh.bsky.social · 03/06/2025

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...

commission.europa.eu

Choose Europe: advance your research career in the EU

Move to the EU as a researcher or scientist. Discover how to relocate, find jobs and funding, and enjoy Europe's excellent quality of life.

000

Nima Rasekh @nimarasekh.bsky.social · 30/05/2025

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.

042

Nima Rasekh @nimarasekh.bsky.social · 28/05/2025

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...

paulkrugman.substack.com

A Letter to Europe

You’re stronger than you think. Act like it.

000

Nima Rasekh @nimarasekh.bsky.social · 24/05/2025

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/...

nytimes.com

Trump Has Cut Science Funding to Its Lowest Level in Decades

The lag in funding extends far beyond D.E.I. initiatives, affecting almost every area of science: chemistry, computing, engineering, materials and more.

000

Nima Rasekh @nimarasekh.bsky.social · 23/05/2025

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.

Nima Rasekh @nimarasekh.bsky.social · 16/04/2025

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!

mpim-bonn.mpg.de

Application for the Guest Program and for postdoc positions | Max Planck Institute for Mathematics

187

Nima Rasekh @nimarasekh.bsky.social · 08/04/2025

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!

020

Nima Rasekh @nimarasekh.bsky.social · 17/03/2025

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

youtube.com

Formalization: Proving Theorems via Computers

YouTube video by Zaiku Group

Nima Rasekh @nimarasekh.bsky.social · 13/03/2025

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...

quantumformalism.academy

Quantum Formalism Academy (QF) - Proving Theorems with Computers

000

Nima Rasekh @nimarasekh.bsky.social · 06/03/2025

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...

mpg.de

Für einen neuen Aufbruch der Wissenschaft

10-Punkte-Plan der Max-Planck-Gesellschaft für die neue Bundesregierung

000

Nima Rasekh @nimarasekh.bsky.social · 04/03/2025

On Thursday (13.3) I am giving a talk in Leaning 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...

linkedin.com

Nima Rasekh on LinkedIn: Leaning In! 2025

Next Thursday (13.3) I'm giving a talk in the Leaning In! 2025 (https://leaning.in/) in Berlin. It is an exciting opportunity to tell people interested in…

Nima Rasekh @nimarasekh.bsky.social · 25/02/2025

(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?

Nima Rasekh @nimarasekh.bsky.social · 05/02/2025

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

dutchcats.github.io

Dutch Categories And Types Seminar

000

Nima Rasekh @nimarasekh.bsky.social · 03/02/2025

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...

021

Nima Rasekh @nimarasekh.bsky.social · 27/01/2025

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...

guyboyde.wordpress.com

TopICS 2024/25

The Topology Intercity Seminar (TopICS) is joint between Utrecht Universiteit, Radboud Universiteit Nijmegen, and Vrije Universiteit Amsterdam. If you wish to receive seminar announcements and/or p…

Nima Rasekh @nimarasekh.bsky.social · 25/01/2025

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

arxiv.org

The Yoneda embedding in simplicial type theory

Riehl and Shulman introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: $(\infty,1)$-category t...

151

Reposted by Nima Rasekh

arxiv math.AT @arxiv-math-at.bsky.social · 15/01/2025

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

011

Reposted by Nima Rasekh

xenaproject.bsky.social @xenaproject.bsky.social · 15/01/2025

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...

youtube.com

Lean Together 2025: Oliver Nash, Root systems and root data in Mathlib

YouTube video by leanprover community

0206

Nima Rasekh @nimarasekh.bsky.social · 18/12/2024

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...

nimarasekh.github.io