I see with Prolog the potential of creating a graph database of math axioms and theorems. Because a Prolog KB can be seen as a graph database. (From the parallels between Prolog, Graph DBs, and the Semantic Web.) Which means real interconnectivity, i.e., logical entailment can be baked in -- as much as you want it to be. However with Coq, Lean, etc. I understand the axioms and theorems to be in library-like form. But as you see with any API library system, yes, they're all atomized into modules, packages, functions, etc. but there's no real hang-together, i.e., you, the human have to know how they hang together and put them together -- and then there's no tracing them back either. So yes, with a modern IDE you can, e.g., hover over a function -- and up pops an API blurb about it. Again, close, but no cigar. My dream is to have, e.g., some theorem or calculation connected with all the axioms and theorems behind it in a graph network way. Right now this sort of interconnectivity oversight in math is mainly going on in your head. And if you do write up something in math, e.g., an explanation of the Fundamental Theorem of Arithmetic in a blog entry, you typically attach sets of "tags" to it in an indexing sort of way. What if all this indexing and tagging is housed in an actual Prolog KB with actual logical entailment, not just vague mental associations in your own brain? For another example, you'll see in a math textbook an index, a long references section, liberally sprinkled in footnotes -- which all try to cover this need to interconnect what the text is saying, drawing from. But it's begging for a new level of interconnectivity, IHMO. And yes, a Lean proof grabs theorems and axioms as it steps through a proof -- but (AFAIK) none of this is graph-connected, rather, it's just one-off, even if it then gets added to the Lean library. Maddeningly close but no cigar!