[HN Gopher] Building the Mathematical Library of the Future
___________________________________________________________________
Building the Mathematical Library of the Future
Author : misotaur
Score : 74 points
Date : 2020-11-11 17:41 UTC (5 hours ago)
(HTM) web link (www.quantamagazine.org)
(TXT) w3m dump (www.quantamagazine.org)
| ahelwer wrote:
| Lean is the basis for my favorite puzzle game of the past five
| years:
| https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...
|
| It's like enemies & bosses are mathematical theorems you have to
| prove. Each time you slay one, you get it as a weapon you can use
| against further, more difficult bosses! The grand finale
| (Inequality World) is very memorable; such a feeling of
| accomplishment after I cracked it all. Then you zoom out and
| realize the math you've defeated reaches, like, fourth grade at
| most.
|
| Lean revolutionized my understanding of math itself, which I
| wrote about here: https://ahelwer.ca/post/2020-04-05-lean-
| assignment/
| dharmatech wrote:
| Video demonstrating what it's like to use Lean interactively:
|
| https://www.youtube.com/watch?v=p4IrbnPomXg
| edgyquant wrote:
| 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 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.
| ezequiel-garzon wrote:
| 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.
| edgyquant wrote:
| It's more something that can tell you if you've already been
| disproven and it would save man hours.
| dddbbb wrote:
| 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.
| Koshkin wrote:
| > _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_?
| mturmon wrote:
| 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
| roywiggins wrote:
| 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)
| yaseer wrote:
| 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 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.
| dddbbb wrote:
| 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.
| auggierose wrote:
| 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.
| raphlinus wrote:
| 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).
| yaseer wrote:
| 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
| _' )
|
| _https://xkcd.com/927/
| dddbbb wrote:
| 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
| carterschonwald wrote:
| Here'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
| breckinloggins wrote:
| 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
| (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.
| AnimalMuppet wrote:
| 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.
| jcranmer wrote:
| 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.
| alanbernstein wrote:
| 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.
| kxyvr wrote:
| This 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...
___________________________________________________________________
(page generated 2020-11-11 23:01 UTC)