3 ms·

Is there such a thing as the graph of lemmas and theorems in mathematics, somewhere online? I can't really understand much of mathematics, but I would apprecia

Is there such a thing as the graph of lemmas and theorems in mathematics, somewhere online? I can't really understand much of mathematics, but I would appreciate seeing the graph of how all major proofs are constructed with help of other proofs.

deleted 2y ago
[deleted]
xanderlewis 2y ago
You mean like a dependency tree? There isn’t a comprehensive one — it would be way too big and we don’t have all mathematical knowledge written down in one place anyway. But if you’re interested in any given classical result, if you ask I’m sure a mathematician can give you a rough idea of what the path back down to first principles is. If you’re not literally interested in starting by assuming the existence of the empty set, say, then opening any introductory book on the topic will give you an idea. Just look at the proof of the result and follow its references back. It won’t go that deep.
- galaxyLogic 2y ago
  I see. I was just thinking I would personally appreciate seeing a big graph of proof-dependencies. A bit like "Seeing the Forest from the Trees". Every mathematician is working on their own TREE, I assume. But might be useful if somebody was looking at how the FOREST is doing.
- lupire 2y ago
  > it would be way too big and we don’t have all mathematical knowledge written down in one place anyway. Yet somehow Google managed to index the Internet. And the human genome is indexed.
jeremyscanvic 2y ago
The thing with mathematics is there are often many different ways to prove things leaving no universally agreed upon graph of true mathematical statements in terms of which helps proving which! That being said, you might want to check out ProofWiki [1], an online collaborative project featuring mathematical proofs consistently linked together. [1] https://proofwiki.org/wiki/Main_Page https://proofwiki.org/wiki/Main_Page
- galaxyLogic 2y ago
  Ah, just what I was asking for. Thanks
reuben364 2y ago
There is a large library of mathematics formalized in lean called mathlib. There are graphs for the module dependencies, but I haven't seen any at the level of definitions (including lemmas and theorems).

deleted 2y ago

[deleted]

xanderlewis 2y ago

You mean like a dependency tree? There isn’t a comprehensive one — it would be way too big and we don’t have all mathematical knowledge written down in one place anyway. But if you’re interested in any given classical result, if you ask I’m sure a mathematician can give you a rough idea of what the path back down to first principles is. If you’re not literally interested in starting by assuming the existence of the empty set, say, then opening any introductory book on the topic will give you an idea. Just look at the proof of the result and follow its references back. It won’t go that deep.

galaxyLogic 2y ago
I see. I was just thinking I would personally appreciate seeing a big graph of proof-dependencies. A bit like "Seeing the Forest from the Trees". Every mathematician is working on their own TREE, I assume. But might be useful if somebody was looking at how the FOREST is doing.
lupire 2y ago
> it would be way too big and we don’t have all mathematical knowledge written down in one place anyway. Yet somehow Google managed to index the Internet. And the human genome is indexed.

jeremyscanvic 2y ago

The thing with mathematics is there are often many different ways to prove things leaving no universally agreed upon graph of true mathematical statements in terms of which helps proving which! That being said, you might want to check out ProofWiki [1], an online collaborative project featuring mathematical proofs consistently linked together. [1] https://proofwiki.org/wiki/Main_Page https://proofwiki.org/wiki/Main_Page

galaxyLogic 2y ago
Ah, just what I was asking for. Thanks

reuben364 2y ago

There is a large library of mathematics formalized in lean called mathlib. There are graphs for the module dependencies, but I haven't seen any at the level of definitions (including lemmas and theorems).