Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Building the Mathematical Library of the Future

quantamagazine.org

Post reply on HN
Print view View original

11–20 of 47 posts

Re: Building the Mathematical Library of the Future

#11

Post by dddbbb »

raphlinus wrote: post #5
yaseer wrote: post #4

There 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…

The author of the Metamath Zero paper is actually one of the most active contributors to the project described in the article[0].

[0]: https://leanprover-community.github.io/mathlib_stats.html

Re: Building the Mathematical Library of the Future

#12

Post by dddbbb »

yaseer wrote: post #4

There 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…

It seems to me like Lean has a lot of the momentum at the moment. It's clear that other projects like Coq suffer from a lack of traditional mathematicians formalising modern, fashionable topics. Kevin Buzzard's implementation in Lean of perfectoid spaces is a great example of that boundary being broken, as far as I can tell the most advanced Coq proofs are the four colour theorem and Feit-Thompson theorem, which have analogue proofs from the 60s and 70s.

Re: Building the Mathematical Library of the Future

#13

Post by mturmon »

ezequiel-garzon wrote: post #7
edgyquant wrote: post #2

I’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.

One of the usual examples given in reaction to this question is the puzzle of Euclid's 5th postulate, the parallel-lines postulate. People tried for centuries to prove that it could be deduced from the other axioms. Turned out, it was independent of the others.

A proof system could identify cases where you need hidden assumptions in order to make proofs. In this case, you would get a null result from the oracle, which would be valuable in itself.

[1] https://en.wikipedia.org/wiki/Parallel_postulate

Re: Building the Mathematical Library of the Future

#14

Post by AnimalMuppet »

breckinloggins wrote: post #8

I 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 (pe…

The tower of theorems may be a graph, but it is not a directed acyclic graph. (You probably want it to be directed, though...)

That is, you want to get to Z? Well, you start at A. But you can get there by the sequence B, D, H, R, Z, or you can get there by B, C, F, H, R, Z, or by B, C, F, J, Q, S, U, Z. There is more than one route to proving many important theorems.

Re: Building the Mathematical Library of the Future

#15

Post by auggierose »

dddbbb wrote: post #12
yaseer wrote: post #4

There 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…

It seems to me like Lean has a lot of the momentum at the moment. It's clear that other projects like Coq suffer from a lack of traditional mathematicians formalising modern, fashionable topics. Kevin Buzzard's implementation in Lean of perfectoid spaces is a great example of that boundary being broken, as far as I can tell the most advanced Coq proofs are the four colour theorem and Feit-Thompson theorem, which have…

But you have to take into account that the Coq proofs are actual proofs of big THEOREMS. What Buzzard has done is implementing a big DEFINITION :-)

Also, the Flyspeck project has formalised the proof of a pretty recent theorem as well, mostly in HOL-Light and Isabelle.

Re: Building the Mathematical Library of the Future

#16

Post by roywiggins »

mturmon wrote: post #13
ezequiel-garzon wrote: post #7

Earlier quoted context omitted.

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.

One of the usual examples given in reaction to this question is the puzzle of Euclid's 5th postulate, the parallel-lines postulate. People tried for centuries to prove that it could be deduced from the other axioms. Turned out, it was independent of the others. A proof system could identify cases where you need hidden assumptions in order to make proofs. In this case, you would get a null result from the oracle, whic…

At best an proof-checker can invalidate a purported proof, it absolutely is not going to prove that no proofs are valid (it would have to affirmatively prove that the result is actually independent of the axioms you picked, which is a lot harder)

Re: Building the Mathematical Library of the Future

#17

Post by Koshkin »

ezequiel-garzon wrote: post #7
edgyquant wrote: post #2

I’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.

> automated proofs

You've got a point, but in this case you are barking at the wrong tree. Aren't they talking about automated proof-checking?

Re: Building the Mathematical Library of the Future

#18

Post by edgyquant »

ezequiel-garzon wrote: post #7
edgyquant wrote: post #2

I’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.

It’s more something that can tell you if you’ve already been disproven and it would save man hours.

Re: Building the Mathematical Library of the Future

#19

Post by jcranmer »

AnimalMuppet wrote: post #14
breckinloggins wrote: post #8

I 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 (pe…

The tower of theorems may be a graph, but it is not a directed acyclic graph. (You probably want it to be directed, though...) That is, you want to get to Z? Well, you start at A. But you can get there by the sequence B, D, H, R, Z, or you can get there by B, C, F, H, R, Z, or by B, C, F, J, Q, S, U, Z. There is more than one route to proving many important theorems.

The actual representation you want wouldn't be a regular graph, but a graph distinguishing theorems and proofs, where the antecedents of theorems are proofs of those theorems, and the antecedents of proofs are theorems they rely on. This kind of graph seems like it should come up regularly enough to have a special name, but I haven't been able to find one.

One important property to note is that a fair number of theorems exist where you can prove A with B or prove B with A, so the underlying directed graph is definitely very cyclic.

Re: Building the Mathematical Library of the Future

#20

Post by alanbernstein »

jcranmer wrote: post #19
AnimalMuppet wrote: post #14

Earlier quoted context omitted.

The tower of theorems may be a graph, but it is not a directed acyclic graph. (You probably want it to be directed, though...) That is, you want to get to Z? Well, you start at A. But you can get there by the sequence B, D, H, R, Z, or you can get there by B, C, F, H, R, Z, or by B, C, F, J, Q, S, U, Z. There is more than one route to proving many important theorems.

The actual representation you want wouldn't be a regular graph, but a graph distinguishing theorems and proofs, where the antecedents of theorems are proofs of those theorems, and the antecedents of proofs are theorems they rely on. This kind of graph seems like it should come up regularly enough to have a special name, but I haven't been able to find one. One important property to note is that a fair number of theor…

Maybe you've encountered it before, but your comment sort of reminds of the concept of a hypergraph (https://en.wikipedia.org/wiki/Hypergraph).

I'm not sure if this is equivalent or related, but I'm imagining an object which can contain, let's call them hypernodes. For example, in the case where A and B mutually imply each other, (A, B) is a hypernode, which internally contains a graph representing the relationship between A and B, but that relationship can be ignored in the main graph. I imagine this would become untenable with a slightly more complex network, though.

Post reply on HN