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.
Jean-Baptiste Vienney (Oct 11 2023 at 23:05):I've recently realized (by looking at what people are doing) that the ultimate system for doing mathematics on a computer would be to combine the technologies of computer algebra systems with those of proof assistants, in order to be able to do formal computations and manipulate mathematical theories at the same time resulting in a system able to help you explore mathematical theories, write proofs, compute automatically, generate textbooks etc...
Many people are working on doing something like this but it looks like a massive work. There is notably the project MathScheme of @Jacques Carette and cie. and the project Theorema of Bruno Buchberger (the guy who discovered Gröbner basis) and cie. Sadly the second one is a package for Mathematica, software which requires to pay a license. As to the first, is there a way to download something and launch it? Are there other systems which are somehow functional, that we can download and try?
My feeling is that these projects are great but it is so much work to create both the theory and the software that there is nothing completely functional today.
Jacques Carette (Oct 11 2023 at 23:27):You are correct that there is nothing completely functional today. MathScheme the project did result in things being implemented, but most of these were experiments to validate technologies "along the way" to such a full-fledged system. I could point you to all sorts of stuff, but you'd be disappointed because none of it is what you're actually looking for.
As it turns out, I'm just back from a week at Dagstuhl where the people who are aiming for such an ultimate system were meeting. We're working on "tetrapodal" systems (see Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal with the actual paper in The Mathematical Intelligencer) that combine computation, deduction, narration, concretization (and organization).
Progress is happening, albeit quite slowly. Many of the same people will be at the HIM Trimester Prospects of Formal Mathematics happening May-August 2024 in Bonn. Applications to attend (fully-funded by HIM) are still open. The list of people who have confirmed they will be there for some period of time is quite impressive.
Jean-Baptiste Vienney (Oct 11 2023 at 23:33):Thank you. I was hesitating to apply to the semester but I think I'm going do it...
Patrick Nicodemus (Oct 12 2023 at 01:49):Assia Mahboubi at Inria is a researcher who works on Coq.
She got a 5 year grant for a project called FRESCO - "Fast and Reliable Symbolic Computation"
https://fresco.gitlabpages.inria.fr/ on joining Coq with computer algebra systems.
I have not really heard anything interesting yet come out of this project so far but I am hoping for cool stuff.
Patrick Nicodemus (Oct 12 2023 at 02:01):For "generating textbooks", there is a plugin for Coq called Alectryon which helps you to embed Coq into mathematical papers.
It has been used here - https://github.com/coq-community/hydra-battles
to create a book based around a Coq library on proof theory (ordinal analysis of Peano arithmetic and similar theories) and discuss/illustrate formal mathematics in TeX.
The book is a living document and is continuously edited as new versions of Coq are released to showcase new features of the language and continuously evolving best practices. Definitely a cool idea.
Michael Kohlhase and Dennis Mueller work on "Semantic TeX" or "sTeX"
https://github.com/slatex/sTeX
which is a LaTeX package for marking up documents with semantic content/meaning.
They are currently researching adding a type system to LaTeX for variables, so you can check the well formedness of mathematical expressions. They are planning to add a theorem prover soon, which should be interesting.
Jean-Baptiste Vienney (Oct 12 2023 at 02:16):Thanks, these projects look very interesting!
I hope that people are going to unite themselves to create some universally accepted software. Something like LaTex that we will all use. Definitely we're not working as math or CS people in a century way.
But there are definitely problems in the academic system to achieve this goal. Like, lot of small teams which work seperately, writing software is not valued on CVs, only published papers and lack of a super funding for the big project. We would need a kind of Manhattan project for creating the tools for doing math in the modern times haha, or if we were Google or Apple, we would have enough money and people which don't care about publications to survive and can work on this. Seriously, for instance, I've already thought to trying to write software but it would have no value on a CV so I don't want to do it.
The trimester looks like a great way to put all the energy together :)
Patrick Nicodemus (Oct 12 2023 at 02:23):Personally I have recently been interested in theorem provers which don't just support one core logic like Coq or Lean but which support multiple logics which can all talk to each other - as long as you can interpret one logic in another or one theory in another, you can translate theorems between logics within the theorem prover. For example you could prove theorems in a weak simple first-order theory using a powerful automated theorem prover and then interpret FOL within set theory to get those theorems about set-theoretic models of the theories.
Now, theorem provers supporting multiple logics have been around for a while. For example, Isabelle supports multiple logics but they don't talk to each other, they're isolated. For this reason most Isabelle users seem to have converged on one single logic (higher order logic) and the other logics supported by Isabelle (ZF, for example) are more neglected.
What I am talking about is natively supporting many different intertranslatable logics, by having a built in notion of what it means to interpret one theory in another or one logic in another. This seems like a more recent and exciting research direction. Here I am thinking of MMT https://uniformal.github.io/doc/philosophy/articles/mmt.pdf
and Dedukti http://www.lsv.fr/~dowek/Publi/expressing.pdf
Patrick Nicodemus (Oct 12 2023 at 02:25):Florian Rabe, the researcher behind MMT, has pointed out several times that you're never going to get mathematicians to universally rally around a single logic. So if you want them to use one universally accepted technology, it has to support multiple logics.
It will be easier for everyone to get behind one theorem prover like MMT if they can use any logic they want.
Jean-Baptiste Vienney (Oct 12 2023 at 02:42):Ok, the paper of Carette and co. agrees with you :)
You should read it. They take a very global view of how computers are used to do mathematics including proving theorems, computing, publishing papers, creating libraries of examples on the internet like OEIS and writing books and how to put everything together. Something like this, they have listed 5 categories which are not very far from this, I don' t rememember exactly. I haven't thought before to all the aspects of math+computer at the same time, just to proving + computing. It' really inspiring :)
Jean-Baptiste Vienney (Oct 12 2023 at 02:47):I would want to encode everything in linear logic. Everything linear at least. But I agree, I should be more open-minded. People want to do linear stuff using set theory and first order logic... as they have always been doing. They should be authorized to do so.
More seriously, translations between different logics is also a great subject from the theoretical point of view and will be illuminating on this side too.
Jean-Baptiste Vienney (Oct 12 2023 at 02:52):People tend not to realize that logic has always been a place where theoretical progress and practical progress are linked together and so it's good for everybody: people who want beautiful theories for the pleasure of human beings and people who just want to encode everything on computers and don't care about human beings. I say this because of the ones who seem scared by computers who would replace them :grinning_face_with_smiling_eyes:
Mike Shulman (Oct 12 2023 at 03:16):Patrick Nicodemus said:
Florian Rabe, the researcher behind MMT, has pointed out several times that you're never going to get mathematicians to universally rally around a single logic. So if you want them to use one universally accepted technology, it has to support multiple logics.
It will be easier for everyone to get behind one theorem prover like MMT if they can use any logic they want.
This is true, but "easier" doesn't necessarily mean "easy". One could just as well say "if you want programmers to use one universally accepted compiler, it has to support multiple programming languages", which is probably true but still unlikely to happen, and arguably not even desirable. I think a better way forward would be to develop translation protocols so that different proof assistants using different logics can interface with each other.
Ryan Wisnesky (Oct 12 2023 at 04:01):The "Hets" toolkit also serves these goals, being a weak meta-system with which to connect stronger systems http://hets.eu
Patrick Nicodemus (Oct 12 2023 at 14:11):@Mike Shulman
Florian Rabe, the researcher behind MMT, has pointed out several times that you're never going to get mathematicians to universally rally around a single logic. So if you want them to use one universally accepted technology, it has to support multiple logics.
It will be easier for everyone to get behind one theorem prover like MMT if they can use any logic they want.This is true, but "easier" doesn't necessarily mean "easy". One could just as well say "if you want programmers to use one universally accepted compiler, it has to support multiple programming languages", which is probably true but still unlikely to happen, and arguably not even desirable. I think a better way forward would be to develop translation protocols so that different proof assistants using different logics can interface with each other.
Yes, I definitely do agree with you that "easier" does not mean "easy." I see that the tone of my post may have undersold the scale of the work and effort needed to do this, there are a lot of unlikely assumptions necessary to make this happen.
Patrick Nicodemus (Oct 12 2023 at 14:39):Jean-Baptiste Vienney said:
I say this because of the ones who seem scared by computers who would replace them :grinning_face_with_smiling_eyes:
This is a bit off topic but my impulse is to interpret this in the context of recent progress in large language models. I apologize for the diversion.
I find it unlikely that a large language model could do many parts of my job as well as I could. However, "as well as I could" may be irrelevant.
I find it increasingly plausible that firms and universities will accept a drastic reduction in the quality of work in exchange for the reduced cost of using AI instead of doing it right.
There is a lot of polarization in the AI discussion, I include myself here. It is a minefield. I see grifters making overzealous and hyperbolic claims about the capabilities and accuracy of LLM's. Certainly the companies pushing it have incentive to lie. Some ML researchers are overstating their claims for publicity. On the other hand the ones warning about the dangers of AI are often using equally ridiculous hyperbole, such as insisting that AI will be able to design its own deadly biochemical weapons.
In discussions with people who are more moderate and see both pros and cons of the LLM's, I still get very concerned and taken aback when they minimize and dismiss the harm of ChatGPT-assisted writing and programming, in the style of "Write me a python script that does this" and then testing it on a couple of inputs to see whether it behaves in the expected way. I really don't think this is a good idea and I am very worried about a collective shift in standards from "You should put forth your best effort to think through your code" to "If it generates correct code 70% of the time, this is enough."
Similarly the dangers to education of students getting explanations of mathematical concepts from ChatGPT and recommending it to others as a learning resource. I don't think ChatGPT can reliably explain mathematical concepts correctly as well as I can, but I do think that universities and tutoring centers will distort that fact and offer ChatGPT assisted learning software.
Patrick Nicodemus (Oct 12 2023 at 14:43):I have a kind of view of society where there is a chain of trust for knowledge. You either know something yourself directly or you trust another individual who claims that it's true. Perhaps they are repeating a claim by someone else they trust and so on. In any case there is an expectation that if you follow this back to the source you have someone who directly has knowledge and evidence for the claim. When there is a breakdown, everyone in the chain up to that point suffers. If we are accepting ChatGPT generated code when we are essentially saying that programmers are no longer responsible or culpable for the correctness or incorrectness of the software, instead this is now left up to chance. Here I do not mean that programmers should verify their code but that they should be responsible for the correctness of their code in the same way that mathematicians are held responsible for the truth of the theorems that they claim and the proofs of the theorems that they claim are correct.
Spencer Breiner (Oct 13 2023 at 00:14):Patrick Nicodemus said:
Michael Kohlhase and Dennis Mueller work on "Semantic TeX" or "sTeX"
https://github.com/slatex/sTeX
which is a LaTeX package for marking up documents with semantic content/meaning.
They are currently researching adding a type system to LaTeX for variables, so you can check the well formedness of mathematical expressions. They are planning to add a theorem prover soon, which should be interesting.
Should obviously be called SemanTeX
Kevin Arlin (Oct 13 2023 at 00:23):Some projects just aren't as advanced on the pun front as we are.
Mike Shulman (Oct 13 2023 at 00:39):I still think tex.stackexchange should have been called OverfullHbox.
Viljami Virolainen (Oct 14 2023 at 20:06):Mike Shulman said:
Patrick Nicodemus said:
Florian Rabe, the researcher behind MMT, has pointed out several times that you're never going to get mathematicians to universally rally around a single logic. So if you want them to use one universally accepted technology, it has to support multiple logics.
It will be easier for everyone to get behind one theorem prover like MMT if they can use any logic they want.This is true, but "easier" doesn't necessarily mean "easy". One could just as well say "if you want programmers to use one universally accepted compiler, it has to support multiple programming languages", which is probably true but still unlikely to happen, and arguably not even desirable. I think a better way forward would be to develop translation protocols so that different proof assistants using different logics can interface with each other.
Kind of something like LLVM, if you squint a bit?
"LLVM is a set of compiler and toolchain technologies that can be used to develop a frontend for any programming language and a backend for any instruction set architecture. LLVM is designed around a language-independent intermediate representation (IR) that serves as a portable, high-level assembly language that can be optimized with a variety of transformations over multiple passes."
https://en.wikipedia.org/wiki/LLVM
Viljami Virolainen (Oct 14 2023 at 20:14):Ryan Wisnesky said:
The "Hets" toolkit also serves these goals, being a weak meta-system with which to connect stronger systems http://hets.eu
Wow, looks pretty impressive!
image.png
