Nima Rasekh

Concretely, we see that many explicit algebraic results, such as Morita invariance for rings and modules, manifest as a special case of very general bicategorical constructions.

This paper was truly a collaborative effort, aimed at understanding very fundamental invariants in (higher) algebra (what Kathryn is after) using higher categorical methods (my world).

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

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

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

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.

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.

A Letter to Europe You’re stronger than you think. Act like it.

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

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.

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.

TLDR: It's a great position with a lot of flexibility, lots of opportunities to meet people, attend conferences, and no teaching duties.

Can't recommend it enough!

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!

Formalization: Proving Theorems via Computers YouTube video by Zaiku Group

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

Für einen neuen Aufbruch der Wissenschaft 10-Punkte-Plan der Max-Planck-Gesellschaft für die neue Bundesregierung

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

GitHub - rzk-lang/sHoTT: Formalisations for simplicial HoTT and synthetic ∞-categories. Formalisations for simplicial HoTT and synthetic ∞-categories. - rzk-lang/sHoTT

TLDR: Formalizing ∞-categories is hard!

There are some proof assistants one can use (both commenced by @emilyriehl.bsky.social ):

- Rzk: github.com/rzk-lang/sHoTT
- Lean: emilyriehl.github.io/infinity-cos...

However, both have their own benefits and drawbacks, one has to deal with!

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

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

(7/7)
- Homotopy type theory (HoTT) is certainly the foundation for some libraries of mainstream proof assistants, such as Coq and Agda.
- Trying to formalize mathematics in HoTT is indeed related to proof relevance, but it does not need to relate to category theory!

(6/7) PS. While I highly recommend the talk, as a homotopy theorist I feel I should offer some context regarding his comments on homotopy type theory:

Machine-Assisted Proofs Machine-Assisted Proofs on Simons Foundation

(5/7) He also gave a Presidential Lecture on Machine-Assisted Proofs at the Simons Foundation, which explores similar themes and is equally accessible to anyone interested:

www.simonsfoundation.org/event/machin...

(4/7) His recent article in the Notices of the AMS is particularly accessible, requiring no background in mathematics or computer science:

www.ams.org/journals/not...

(3/7) Interestingly, one person who shares a similar perspective is Terry Tao, who has written and spoken eloquently about recent developments and future possibilities.

(2/7) Ideally, one would hope for a synthesis of these two fields—something still in its early stages but with the potential to be highly constructive.

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

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…

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

sHoTT is a modern foundation by Emily Riehl & Mike Shulman designed to study and formalize ∞-categories, via the newly developed proof assistant Rzk.

So this line of work not only gives us elegant proofs, but also formalized ∞-category theory libraries applicable to research, teaching, ... .