A working group of about 20 researchers has formed to investigate computational aspects of the methodology ‘toposes as bridges’, with particular reference to the proof-theoretic equivalences established in Chapters 3 and 8 of my book Theories, Sites, Toposes: Relating and studying mathematical theories through topos-theoretic ‘bridges’ and described in these slides.
The organizer is Laurent Lafforgue, and the meetings will take place at the Huawei Lagrange Center for Mathematics and Computation in Paris, starting from the first one, which has happened today.
A final goal is to implement these techniques on a computer, to automatically generate mathematical results by exploiting the capacity of ‘bridges’ to significantly transform the level of complexity of notions and results. Back in 2010, when I first evoked this possibility in the paper The unification of Mathematics via Topos Theory, that idea was regarded with a lot of skepticism, as something almost too good to be true. Now, the time is ripe to start making that dream into reality.
@ocaramello Hi, can you please give some link to this working group? Is it possible to see some of their papers? I would like to know more about your results on this specific idea ˆˆ.
Hi Ricardo, thanks for your question. That working group has broadened its scope and the meetings have touched different aspects of toposes relevant for computer science. No official paper from the working group has been issued yet; I can anticipate that a joint paper with Lafforgue on computing fibred products of toposes and comma toposes should become available in the next months. The talks and discussions have been recorded, but I do not know if the Lagrange Center will make them publicly available; I will alert you in case.