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

0likes483downloads

rootexperimentspremise_retrieval_results.json

premise_retrieval_results.json86 linesDownload Raw Back to experiments

1{2  "Random": {3    "AUC": 0.4988464624381927,4    "R@10": 0.13489873938604055,5    "R@50": 0.675421720785031,6    "MRR": 0.5177648872389418,7    "AUC_ci_lo": 0.4976579056909061,8    "AUC_ci_hi": 0.5025447127337402,9    "R@10_ci_lo": 0.13314589782962657,10    "R@10_ci_hi": 0.13807478534717094,11    "R@50_ci_lo": 0.6708032287760948,12    "R@50_ci_hi": 0.6822757937354658,13    "MRR_ci_lo": 0.5097106183497658,14    "MRR_ci_hi": 0.530494807200449315  },16  "Same module": {17    "AUC": 0.563252943150883,18    "R@10": 0.17701251024723705,19    "R@50": 0.6434465696480249,20    "MRR": 0.9972,21    "AUC_ci_lo": 0.5611102003189763,22    "AUC_ci_hi": 0.5651486253506915,23    "R@10_ci_lo": 0.17269307941264872,24    "R@10_ci_hi": 0.18132900160478696,25    "R@50_ci_lo": 0.6354730399715295,26    "R@50_ci_hi": 0.6551981898656606,27    "MRR_ci_lo": 0.9961949999999999,28    "MRR_ci_hi": 0.998129  },30  "Same namespace": {31    "AUC": 0.5902006516951351,32    "R@10": 0.2200081147938892,33    "R@50": 0.6626223704593136,34    "MRR": 0.9695453174603176,35    "AUC_ci_lo": 0.5880529846813214,36    "AUC_ci_hi": 0.5924840785351329,37    "R@10_ci_lo": 0.21586994086758424,38    "R@10_ci_hi": 0.22475987434791297,39    "R@50_ci_lo": 0.6548427218687078,40    "R@50_ci_hi": 0.6734164434880273,41    "MRR_ci_lo": 0.9664740277777778,42    "MRR_ci_hi": 0.972481648809523843  },44  "Same community": {45    "AUC": 0.7675738080569178,46    "R@10": 0.2066798209803219,47    "R@50": 0.8225669566396177,48    "MRR": 0.889924414802174,49    "AUC_ci_lo": 0.7636466473774499,50    "AUC_ci_hi": 0.7701280102171949,51    "R@10_ci_lo": 0.20206740759955272,52    "R@10_ci_hi": 0.2099666022599327,53    "R@50_ci_lo": 0.8168676201838171,54    "R@50_ci_hi": 0.8301017721564548,55    "MRR_ci_lo": 0.8825203088999172,56    "MRR_ci_hi": 0.896835856295332257  },58  "Network features": {59    "AUC": 0.9910488074402863,60    "R@10": 0.5200779274690902,61    "R@50": 0.9440300907986493,62    "MRR": 0.9978666666666666,63    "AUC_ci_lo": 0.9906065336840136,64    "AUC_ci_hi": 0.9915709117833958,65    "R@10_ci_lo": 0.513202566369347,66    "R@10_ci_hi": 0.5287072912456959,67    "R@50_ci_lo": 0.9401626991702056,68    "R@50_ci_hi": 0.9492015962873687,69    "MRR_ci_lo": 0.9969158333333333,70    "MRR_ci_hi": 0.998671  },72  "All features": {73    "AUC": 0.9935149509905005,74    "R@10": 0.5246824912435099,75    "R@50": 0.944575070939189,76    "MRR": 0.9984,77    "AUC_ci_lo": 0.9931381533391922,78    "AUC_ci_hi": 0.9938923361368286,79    "R@10_ci_lo": 0.51749162029253,80    "R@10_ci_hi": 0.5334405006567039,81    "R@50_ci_lo": 0.9407193927667646,82    "R@50_ci_hi": 0.9497068095655786,83    "MRR_ci_lo": 0.9975475,84    "MRR_ci_hi": 0.99985  }86}