Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
2
datasets available to search
ShareScore release 0.9.0
Dataset results
2 results for “Formal Mathematics”
MLFMF: Data Sets for Machine Learning for Mathematical Formalization
<h3>MLFMF</h3><p><strong>MLFMF (Machine Learning for Mathematical Formalization) </strong>is a collection of data sets for benchmarking recommendation systems used to support formalization of mathematics with proof assistants. These systems help humans identify which previous entries (theorems, constructions, datatypes, and postulates) are relevant in proving a new theorem or carrying out a new construction. </p><p>The MLFMF data sets provide solid benchmarking support for further investigation of the numerous machine learning approaches to formalized mathematics. With more than 250,000 entries in total, this is currently the largest collection of formalized mathematical knowledge in machine learnable format. </p><p>In addition to benchmarking the recommendation systems, the data sets can also be used for benchmarking <strong>node classification</strong> and <strong>link prediction</strong> algorithms. </p><h3>The four data sets</h3><p>Each data set is derived from a library of formalized mathematics written in proof assistants <a href="https://agda.readthedocs.io/en/v2.6.4/"><i>Agda</i></a> or <a href="https://lean-lang.org/"><i>Lean</i></a>. The collection includes </p><ol><li>the largest Lean 4 library <a href="https://github.com/leanprover-community/mathlib4"><strong>Mathlib</strong></a>,</li><li>the three largest Agda libraries:<ul><li>the <a href="https://github.com/agda/agda-stdlib"><strong>standard library</strong></a></li><li>the library of univalent mathematics <a href="https://github.com/UniMath/agda-unimath"><strong>Agda-unimath</strong></a>, and</li><li>the <a href="https://github.com/martinescardo/TypeTopology"><strong>TypeTopology</strong></a> library.</li></ul></li></ol><p>Each data set represents the corresponding library in two ways: as a heterogeneous network, and as a list of syntax trees of all the entries in the library. The network contains the (modular) structure of the library and the references between entries, while the syntax trees give complete and easily parsed information about each entry.</p><p>The Lean library data set was obtained by converting <strong>.olean</strong> files into s-expressions (see the <a href="https://github.com/andrejbauer/lean2sexp"><strong>lean2sexp</strong></a> tool).</p><p>The Agda data sets were obtained with an <a href="https://github.com/andrejbauer/agda/tree/master-sexp">s-expression extension</a> of the official Agda repository (use either master-sexp or release-2.6.3-sexp branch).</p><p>For more details, see our <a href="https://arxiv.org/abs/2310.16005"><strong>arXiv copy</strong></a><strong> </strong>of the paper.</p><h3>Directory structure</h3><p>First, the <strong>mlfmf.zip</strong> archive needs to be unzipped. It contains a separate directory for every library (for example, the standard library of Agda can be found in the stdlib directory) and some auxiliary files. Every library directory contains</p><ul><li>the <strong>network file</strong> from which the heterogeneous network can be loaded,</li><li>a zip of the <strong>entries directory</strong> that contains (many) files with abstract syntax trees. Each of those files describes a single entry of the library.</li></ul><p>In addition to the auxiliary files which are used for loading the data (and described below), the zipped sources of lean2sexp and Agda s-expression extension are present.</p><h4>Loading the data</h4><p>In addition to the data files, there is also a simple python script <strong>main.py</strong> for loading the data. To run it, you will have to install the packages listed in the file <strong>requirements.txt</strong>: <strong>tqdm</strong> and <strong>networkx</strong>. The easiest way to do so is calling <i><strong>pip install -r requirements.txt</strong></i>.</p><p>When running <strong>main.py </strong>for the first time, the script will unzip the entry files into the directory named <strong>entries</strong>. After that, the script loads the syntax trees of the entries (see the <strong>Entry</strong> class) and the network (as <i>networkx.MultiDiGraph</i> object).</p><p><i>Note. The entry files have extension <strong>.dag </strong>(directed acyclic graph), since Lean uses node sharing, which breaks the tree structure (a shared node has more than one parent node).</i></p><h3>More information</h3><p>For more information about the <strong>data collection process</strong>, <strong>detailed data (and data format) description</strong>, and <strong>baseline experiments</strong> that were already performed with these data, see our <a href="https://arxiv.org/abs/2310.16005"><strong>arXiv copy</strong></a><strong> of the paper</strong>.</p><p>For the code that was used to perform the experiments and data format description, visit our github repository <a href="https://github.com/ul-fmf/mlfmf-data"><strong>https://github.com/ul-fmf/mlfmf-data.</strong></a></p><h3>Funding</h3><p>Since not all the funders are available in the Zenodo's database, we list them here:</p><ol><li>This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0024.</li><li>The authors also acknowledge the financial support of the Slovenian Research Agency via the research core funding No. P2-0103 and No. P1-0294.</li></ol><p> </p>
Resources for the article "Investigating the role of educational robotics in formal mathematics education"
<p>This repository contains the material required to reproduce the study looking to investigate the role of educational robotics in formal mathematics education for 15 year old students in the French speaking region of Switzerland. This includes :</p> <ul> <li> <p>Pedagogical content in the form of both teacher and student resources</p> </li> <li> <p>Data collection ressources (surveys and tests)</p> </li> </ul> <p>If you use any of the resources provided in this repository, please cite the following</p> <p>• The Zenodo repository, DOI: 10.5281/zenodo.4649842</p> <p>• The corresponding article : Brender, J., El-Hamamsy, L., Bruno, B., Chessel-Lazzarotto, F., Zufferey, J.D., Mondada, F. (2021). Investigating the Role of Educational Robotics in Formal Mathematics Education: The Case of Geometry for 15-Year-Old Students. In: De Laet, T., Klemke, R., Alario-Hoyos, C., Hilliger, I., Ortega-Arranz, A. (eds) Technology-Enhanced Learning for a Free, Safe, and Sustainable World. EC-TEL 2021. Lecture Notes in Computer Science(), vol 12884. Springer, Cham. https://doi.org/10.1007/978-3-030-86436-1_6</p> <p>• Licence : CC-BY</p>
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.