Building the Mathematical Library of the Future
quantamagazine.org
Building the Mathematical Library of the Future
1–10 of 47 posts
Re: Building the Mathematical Library of the Future
#2I’ve long awaited the day we have automated proof checking. As someone who started in CS but went for a degree in Mathematics I held on to the idea of some sort of test suite that newer mathematicians (who have tend to come up with already existing or already disproven proofs for fun while thinking they’re on to something) could run to determine if they’re wasting their time and it not have to be a class mate making fun of them (sadly I’ve done this to kids who were just excited to try and learn, as if I had any room to talk.)
And it would only scale from there, hell we could run such a test suite against all known proofs and who knows how many ancient theorems we could disprove. I don’t think this is the test suite but something like it and the ANN that OpenAI build to check proofs is a good start.
Re: Building the Mathematical Library of the Future
#3Here’s a nice paper and talk by the mathlib folks at a January 2020 proofs and certified programs conf https://popl20.sigplan.org/details/CPP-2020-papers/14/The-Le...
Might be fun reading for folks
Re: Building the Mathematical Library of the Future
#4There are several proof assistants trying to do what lean is doing (Coq, Isabelle to name but a few). Some of them have very well funded research projects with similar goals: https://cordis.europa.eu/project/id/742178
When programming 'business logic', the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem.
With computer aided proofs, I do wonder if the multitude of systems trying to create a mathematical library of Alexandria is a good thing.
Essentially they're re-formalising the same theorems across different languages. Certainly some languages will model a specific problem better, but it does feel like a duplication of effort.
Re: Building the Mathematical Library of the Future
#5There are several proof assistants trying to do what lean is doing (Coq, Isabelle to name but a few). Some of them have very well funded research projects with similar goals: https://cordis.europa.eu/project/id/742178 When programming 'business logic', the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem. With computer aided proofs, I do wonder if the multitu…
There is work on making proofs portable from one system to another. One effort is Dedukti, which is based on the idea that "lambda pi modulo" is a universal logic for theorem provers. A less ambitious effort is OpenTheory, which from what I can tell is mostly about being able to interoperate between different HOL flavors.
And one of the efforts I personally find most interesting is Metamath Zero, which attempts to be an interchange format among other things, with connections to HOL and Lean. See section 5 of: https://arxiv.org/abs/1910.10703
I think there are many provers which theoretically could be used for this effort, and am not convinced Lean is the absolute best, but I applaud the community for actually going ahead and doing it, instead of farting around with tools and hoping the library will magically happen (a valid critique of HoTT in my opinion).
Re: Building the Mathematical Library of the Future
#6There are several proof assistants trying to do what lean is doing (Coq, Isabelle to name but a few). Some of them have very well funded research projects with similar goals: https://cordis.europa.eu/project/id/742178 When programming 'business logic', the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem. With computer aided proofs, I do wonder if the multitu…
There is work on making proofs portable from one system to another. One effort is Dedukti, which is based on the idea that "lambda pi modulo" is a universal logic for theorem provers. A less ambitious effort is OpenTheory, which from what I can tell is mostly about being able to interoperate between different HOL flavors. And one of the efforts I personally find most interesting is Metamath Zero, which attempts to be…
Thanks for sharing! I Remember seeing Dedukti a while back, but I haven't seen some of these newer translation efforts.
I do hope the translation systems are actively used to consolidate, rather than built as an academic exercise.
There seems to be a large gap between vision ('our project will encapsulate all of mathematics in one place') and reality ('our project will just proliferate another standard')
Re: Building the Mathematical Library of the Future
#7I’ve long awaited the day we have automated proof checking. As someone who started in CS but went for a degree in Mathematics I held on to the idea of some sort of test suite that newer mathematicians (who have tend to come up with already existing or already disproven proofs for fun while thinking they’re on to something) could run to determine if they’re wasting their time and it not have to be a class mate making…
What do you gain from automated proofs? Take the infinitude of primes. Plenty of textbooks different proofs of this fact to deepen your insight. Having an oracle-like entity tell me whether something is true or false is unlikely to have the same result, and I’m afraid “following the automated proof” won’t help much in this regard.
Re: Building the Mathematical Library of the Future
#8I wonder if in addition to the proofs this could also be used to provide generated "meta textbooks". The towers of theorems must be a graph, right? So shouldn't I be able to say "I want to understand Calabi–Yau manifolds" and get a custom-made exercise set all the way down to set theory?
Add an invertible "examples" generator so examples can become exercises and keep track of all the exercises you've already done (perhaps with some kind of spaced-repetition system built in) and you can just keep "fleshing out" your own graph of practiced math knowledge starting with wherever you want to look next.
Re: Building the Mathematical Library of the Future
#9This is actually pretty cool. Every time theorem proving comes up, I make some mild complaints about not having any examples from real analysis or calculus like the mean value theorem. They in fact do and they can be found here [1]. Personally, I don't find it particularly easy to read, but I am appreciative that there are some good examples of proofs that more people would be familiar with than, for example something from number theory.
[1] https://leanprover-community.github.io/mathlib_docs/analysis...
Re: Building the Mathematical Library of the Future
#10I’ve long awaited the day we have automated proof checking. As someone who started in CS but went for a degree in Mathematics I held on to the idea of some sort of test suite that newer mathematicians (who have tend to come up with already existing or already disproven proofs for fun while thinking they’re on to something) could run to determine if they’re wasting their time and it not have to be a class mate making…
What do you gain from automated proofs? Take the infinitude of primes. Plenty of textbooks different proofs of this fact to deepen your insight. Having an oracle-like entity tell me whether something is true or false is unlikely to have the same result, and I’m afraid “following the automated proof” won’t help much in this regard.
Increased assurance that the proof is correct and the various standard benefits of digital over analogue data. This software automatically checks the validity of the proof (with a very small, manually verified core of code doing so), it does not automatically generate proofs wholesale. The proof itself is written by the mathematician interactively, which is still a manual process that requires skill, creativity and thought.