Datasetpublic

MathNetwork/MathlibGraph

MathlibGraph: The Multinetwork of Mathlib Dependency graph of Mathlib (commit 534cf0b, 2 Feb 2026), the largest formal mathematics library for Lean 4 (v4.28.0-rc1). Three dependency layers (declarations, modules, namespaces), each with nodes, edges, and precomputed network metrics. Quick Stats Declarations Modules Namespaces (k=2) Nodes 308,129 7,564 10,097 Edges 8,436,366 20,881 332,081 (weighted) DAG depth 83 154 7 (after SCC condensation)… See the full description on the dataset page: https://huggingface.co/datasets/MathNetwork/MathlibGraph.

sourceHugging Faceapache-2.0updated 6mo agoView on Hugging Face

0likes466downloads

rootexperimentsholdout_decl_level.json

holdout_decl_level.json113 linesDownload Raw Back to experiments

1{2  "completed_splits": [3    {4      "seed": 42,5      "results_uniform": {6        "Random": {7          "AUC": 0.5003,8          "R@10": 0.1333,9          "R@50": 0.676,10          "MRR": 0.524,11          "n_problems": 500012        },13        "Same module": {14          "AUC": 0.563,15          "R@10": 0.1789,16          "R@50": 0.642,17          "MRR": 0.998,18          "n_problems": 500019        },20        "Same namespace": {21          "AUC": 0.5922,22          "R@10": 0.2233,23          "R@50": 0.664,24          "MRR": 0.966,25          "n_problems": 500026        },27        "Same community": {28          "AUC": 0.5,29          "R@10": 0.0683,30          "R@50": 0.618,31          "MRR": 1.0,32          "n_problems": 500033        },34        "Network features": {35          "AUC": 0.9778,36          "R@10": 0.5124,37          "R@50": 0.937,38          "MRR": 0.997,39          "n_problems": 500040        },41        "All features": {42          "AUC": 0.9844,43          "R@10": 0.5212,44          "R@50": 0.94,45          "MRR": 0.997,46          "n_problems": 500047        }48      },49      "results_hard": {50        "Random": {51          "AUC": 0.5003,52          "R@10": 0.1333,53          "R@50": 0.676,54          "MRR": 0.524,55          "n_problems": 500056        },57        "Same module": {58          "AUC": 0.563,59          "R@10": 0.1789,60          "R@50": 0.642,61          "MRR": 0.997,62          "n_problems": 500063        },64        "Same namespace": {65          "AUC": 0.5922,66          "R@10": 0.2234,67          "R@50": 0.664,68          "MRR": 0.964,69          "n_problems": 500070        },71        "Same community": {72          "AUC": 0.5,73          "R@10": 0.0683,74          "R@50": 0.618,75          "MRR": 1.0,76          "n_problems": 500077        },78        "Network features": {79          "AUC": 0.9776,80          "R@10": 0.5097,81          "R@50": 0.937,82          "MRR": 0.997,83          "n_problems": 500084        },85        "All features": {86          "AUC": 0.9842,87          "R@10": 0.5191,88          "R@50": 0.94,89          "MRR": 0.997,90          "n_problems": 500091        }92      },93      "diagnostics": {94        "in_degree_pearson_r": 0.999851,95        "out_degree_pearson_r": 0.999315,96        "pagerank_pearson_r": 0.950683,97        "betweenness_pearson_r": 0.712134,98        "community_nmi": 0.7821,99        "dag_layer_mean_shift": 2.9912,100        "test_decl_mean_in_degree": 0.0,101        "test_decl_mean_out_degree": 0.0,102        "test_decl_mean_pagerank": 7.667e-07,103        "n_wcc": 48812,104        "largest_wcc_size": 259311,105        "g_train_edges": 6727267,106        "edges_removed_pct": 20.21107      },108      "n_train_decls": 194929,109      "n_test_decls": 48733,110      "elapsed_s": 2396111    }112  ]113}