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

41–47 of 47 posts

Re: Building the Mathematical Library of the Future

#41

Post by [deleted] »

jcranmer wrote: post #28
drdeca wrote: post #24

Earlier quoted context omitted.

Is the name you are looking for "bipartite directed graph" ? Well, specifically, a bipartite directed graph equipped with the specific partition, but if the graph is connected[1], which it should be in this case, then the partition is uniquely defined. I guess such a graph would define another directed graph which has as vertices, the subsets of the "theorem" vertices, and a directed edge from any such subset to anot…

> Is the name you are looking for "bipartite directed graph" ? I've described it as bipartite directed graph in the past, but a key element of what I describe is that the two sets of nodes generally inherit their properties in different ways. For one set, you need something to happen "for all" predecessors; for the other, it needs to happen "for any" predecessor. It's this extra property I have no name for.

[deleted]

Re: Building the Mathematical Library of the Future

#42

Post by yaseer »

delusional wrote: post #35
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…

The exact same thing is said about other programming languages.

I agree, and discussed this a little.

There is one key difference with the theorem provers- many of them share this lofty goal of building a library, akin to a 'library of Alexandria' (The article discusses this vision, and the research project I linked to at Cambridge is called 'Alexandria').

It's a grand vision - to formalise all mathematical knowledge in a library.

This vision doesn't exist in the world of regular software.

Nobody to my mind has claimed they're building a library of Alexandria. You could make the claim for npm, but I might shed a tear if you did that.

Re: Building the Mathematical Library of the Future

#43

Post by ahelwer »

emrehan wrote: post #40
ahelwer wrote: post #21

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. The…

How many hours does it take to complete?

I'd say 10 or so?

Re: Building the Mathematical Library of the Future

#44

Post by cmehdy »

ahelwer wrote: post #21

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. The…

Thank you for sharing this, I'm having a lot of fun with it!

I've been approaching proofs from a different angle, going through the book "How to prove it" and making a complicated setup to use an old applet recommended in the book (ProofDesigner, which requires old versions of Firefox to even load the applet). While that part helps with formal symbols, it's very rigid and aging compared to this fantastic resource and language.

Re: Building the Mathematical Library of the Future

#45

Post by alanbernstein »

The_rationalist wrote: post #26
alanbernstein wrote: post #20

Earlier quoted context omitted.

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…

A graph whose nodes have for attributes graphs are not an hypergraph. Hypergraph do not modify the definition of a node, only the definition of an (hyper) edge. From the best AGI project out there: A hypergraph is much like a graph, except that the edges, now called “hyperedges” can contain more than two vertexes. That is, the hyperedge, rather than being an ordered pair of vertexes, is an ordered list of vertexes. T…

Thanks for the clarification, that makes sense. I just would not have been surprised to learn that two different looking extensions of the basic graph concept might turn out to be equivalent, or dual.

Re: Building the Mathematical Library of the Future

#46

Post by Ericson2314 »

digama0 wrote: post #36
Ericson2314 wrote: post #33

Earlier quoted context omitted.

I think the "imperative" part is the tactics—metaprogram invocations, the underlying language is still functional. Idris is geared more towards programming than theorem proving, with the difference basically being that with the latter one cares about more than the types ("I didn't formalize my spec completely") so the specific inhabitant matters. That makes tactics a bit dangerous. Now there is also a school of thoug…

> implementation in C++ rather than a nice functional language for dogfooding To be fair, the main author of Lean has been cloistered for two years writing the next version, Lean 4, which is written in its own (pure functional) language. The siren song is strong :)

Oh, I did not know that! Will check it out.

Re: Building the Mathematical Library of the Future

#47

Post by carapace »

ahelwer wrote: post #21

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. The…

Oh man that was fun! Totally nerd-sniped my day though.

Got me to go back and re-watch Kevin Buzzard's talk at MS Research in re: Lean, "The Future of Mathematics?"

https://www.youtube.com/watch?v=Dp-mQ3HxgDE

https://news.ycombinator.com/item?id=21200721

Post reply on HN