You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
John Baez (Jul 13 2021 at 21:02):Here at the Topos Institute, Valeria de Paiva and Brendan Fong are starting a project to organize mathematical knowledge.
It's just starting! But the idea is to use software to read mathematical texts and build up a hierarchy of concepts.
John Baez (Jul 13 2021 at 21:03):This project is necessary, because the mathematical literature is growing faster than anyone can keep up with it. It's getting harder and harder to find the results you need. It's time to apply modern technology to this problem!
John Baez (Jul 13 2021 at 21:04):Check out what Valeria and Brendan have done so far:
You can help annotate abstracts of papers to improve their ontology of mathematics! You can leave suggestions and questions on their blog. Or maybe you can even join the project!
John Baez (Jul 13 2021 at 21:05):
Henry Story (Jul 13 2021 at 21:05):Will they also be looking at integrating knowledge form libraries such as Lean or Agda?
John Baez (Jul 13 2021 at 21:07):Ask on their blog article! They're the ones who know what they're planning to do.
Henry Story (Jul 13 2021 at 21:12):done!
Valeria de Paiva (Jul 14 2021 at 20:55):Sorry @Henry Story I only saw the question today! and I replied on the blog, but no. Integrating proof assistants libraries is a lot of hard work! we're not proof assistants people!
Henry Story (Jul 14 2021 at 20:56):I guess it depends how much funds you get :-)
Valeria de Paiva (Jul 14 2021 at 21:08):well, to a certain extent everything in life depends on how much funds you've got. But here there's a question of principle too: I do not have a good theory of how to put together the different foundational bases of various proof assistants. "Institutions" are definitely not enough.
Henry Story (Jul 14 2021 at 21:10):Do you need that, or would something that can search those libraries and point people to some good guesses be enough?
Henry Story (Jul 14 2021 at 21:11):I mean you can't have a parser for human language yet that is complete, so I guess you are building something more like a search engine.
Henry Story (Jul 14 2021 at 21:12):But one that has some conceptual modelling that is aware of mathematical concepts.
Valeria de Paiva (Jul 14 2021 at 21:24):As I said I'm not a proof assistant person, but my understanding is that simply to put things in one environment is hard enough--as mentioned both by Larry Paulson in his Topos colloquium talk and by Florian Rabe in his contribution to "Every Proof Assistant".
Henry Story (Jul 14 2021 at 21:26):yes, I trust you that it is not easy. (And I watched that talk by Rabe)
Just there is a lot of computer accessible data there with proofs...
Still I find google scholar with its simple search engine really to be the most useful tool around when doing research.
Valeria de Paiva (Jul 14 2021 at 21:35):We have good enough parsers for human languages: we cannot reason with what they produce, they don't have the precision we require, but their recall is good and it's getting better. Thinking of mathematics as a "foreign language" makes some sense. Google Scholar is not the only game in town, if the data was freely available, there would be other players. as it is, people are making do with the data there is.
Jon Awbrey (Jul 15 2021 at 12:08):Hi @Valeria de Paiva , I'll go ahead and share my comment here as fodder for potential discussion.
You may wish to look into the model of knowledge development proposed in my work on Inquiry Driven Systems.
I've been a participant∫observer in webontology knowledge projects for a couple of decades now and they always give far more attention to knowledge as a product than due reflection on the dynamics of inquiry required to develop that provisional knowledge. Many such projects have come and gone, and it's my guess that bias is one of the reasons.
So I've been working on that …
Jon
Javier Prieto (Jul 15 2021 at 12:40):I wonder if deep language models would be useful for this. I know that GPT-3 has been fine tuned to suggest Lean tactics and to search paper databases (presumably thanks to fuzzy semantic matching), so the pieces seem to be there already.
Valeria de Paiva (Jul 16 2021 at 00:20):Thanks again @Jon Awbrey ! I have seen your suggestion and it's in the pile of things to read. But we don't want a new theory, we want to use off-the-shelf tools, as much as possible.
Valeria de Paiva (Jul 16 2021 at 00:22):And yes @Javier Prieto GPT-3 and all its friends might very well be useful, but we're hoping to get by with quite a bit less. Language models are two a penny these days, we might as well use them.
Jon Awbrey (Jul 16 2021 at 03:15):Valeria de Paiva said:
Thanks again Jon Awbrey ! I have seen your suggestion and it's in the pile of things to read. But we don't want a new theory, we want to use off-the-shelf tools, as much as possible.
I hear ya. Best regards, Jon