More and more often, different foundations of mathematics emerging. In some cases, they even rebuild classical theorems (e.g. number theory, Cartan geometry [1].. etc) on top of it. Some foundations have the merit that theorems seem to be more easily checked by computer programs, see [1] for example. This is certainly exciting to me. However, a concern naturally arises as in other subjects: the size of the community.

That makes me wonder, is there anyone working on translating theorems from one to another, so that people prove B' based on B can still contribute to that based on A? After all, the community based on ZFC has much longer history.. and I don't think it's practical to reconstruct all of them "manually".

  • [1] Formalizing Cartan Geometry in Modal Homotopy Type Theory-[Felix Wellen]


You must log in to answer this question.