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.
That sounds quite interesting. I will wait then. Thank you! Nevertheless, I want to insist maybe concretely: I am very interested in the idea exposed In the last slide "Automatic Generation of Theorems" of the talk “Toposes as ‘bridges’ for mathematics and artificial intelligence”. I myself like to play with Automated Theorem Provers and if there is some work you may be able to point to for further reading I would gladly follow the recommendation. Otherwise, if there is a paper of yours in which that idea is exposed at a greater level, I would like to know it.
In category theory, a Grothendieck topology is a structure on a category C that makes the objects of C act like the open sets of a topological space. A category together with a choice of Grothendieck topology is called a site1.
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 slides23.
I hope this helps! Let me know if you have any other questions.
