size_categories:n<1K format:parquet modality:text library:datasets library:pandas library:mlcroissant library:polars library:distilabel region:us synthetic distilabel rlaif
---
size_categories: n<1K
dataset_info:
  features:
  - name: informal_statement
    dtype: string
  - name: formal_statement
    dtype: string
  - name: distilabel_metadata
    struct:
    - name: raw_output_proof_generator
      dtype: string
  - name: model_name
    dtype: string
  - name: natural_language
    dtype: string
  - name: analysis
    dtype: string
  - name: assessment
    dtype: string
  - name: proof
    dtype: string
  splits:
  - name: train
    num_bytes: 23786
    num_examples: 10
  download_size: 27648
  dataset_size: 23786
configs:
- config_name: default
  data_files:
  - split: train
    path: data/train-*
tags:
- synthetic
- distilabel
- rlaif
---

<p align="left">
  <a href="https://github.com/argilla-io/distilabel">
    <img src="https://raw.githubusercontent.com/argilla-io/distilabel/main/docs/assets/distilabel-badge-light.png" alt="Built with Distilabel" width="200" height="32"/>
  </a>
</p>

# Dataset Card for test_deepseek_prover

This dataset has been created with [distilabel](https://distilabel.argilla.io/).


The pipeline script was uploaded to easily reproduce the dataset:
[pipe_deepseek_prover.py](https://huggingface.co/datasets/plaguss/test_deepseek_prover/raw/main/pipe_deepseek_prover.py).

It can be run directly using the CLI:

```console
distilabel pipeline run --script "https://huggingface.co/datasets/plaguss/test_deepseek_prover/raw/main/pipe_deepseek_prover.py"
```


## Dataset Summary

This dataset contains a `pipeline.yaml` which can be used to reproduce the pipeline that generated it in distilabel using the `distilabel` CLI:

```console
distilabel pipeline run --config "https://huggingface.co/datasets/plaguss/test_deepseek_prover/raw/main/pipeline.yaml"
```

or explore the configuration:

```console
distilabel pipeline info --config "https://huggingface.co/datasets/plaguss/test_deepseek_prover/raw/main/pipeline.yaml"
```

## Dataset structure

The examples have the following structure per configuration:


<details><summary> Configuration: default </summary><hr>

```json
{
    "analysis": "1. Relevance to Current Research: This statement is related to basic number theory and combinatorics, which are well-established areas of mathematics. While it may not be directly addressing a currently researched problem, it could be a useful lemma or intermediate result in a larger proof. Score: above average.\n2. Complexity and Depth: The statement is relatively simple, and the proof is likely to involve basic algebraic manipulations and properties of factorials. It may not challenge existing theories or methodologies, but it could provide a useful insight or application. Score: fair.\n3. Interdisciplinary Potential: This statement is primarily focused on number theory and combinatorics, with limited potential for interdisciplinary connections. Score: poor.\n4. Community Needs and Gaps: This statement may fill a gap in the Lean4 library by providing a useful lemma or intermediate result, but it does not address a specific need or gap in the community. Score: fair.\n5. Innovativeness: The statement does not propose new methods, concepts, or applications, and is likely a known result in number theory. Score: poor.",
    "assessment": "above average",
    "distilabel_metadata": {
        "raw_output_proof_generator": "```lean4\ntheorem mathd_number_theory_1 (n m : \u2115) (h : n \u2264 m) : n! * n ^ (m - n) \u2264 m! :=\nbegin\n  induction m with k hk generalizing n,\n  { cases n, { refl }, { cases h } },\n  cases n,\n  { simp, },\n  { have h\u0027 : n \u2264 k := le_of_lt (lt_of_le_of_lt h (nat.lt_succ_self k)),\n    have := hk n h\u0027,\n    rw [nat.factorial_succ, nat.factorial_succ] at this,\n    have := mul_le_mul this (pow_le_pow_of_le_left (le_refl _) (le_of_lt (nat.lt_succ_self _))),\n    simp at this,\n    assumption }\nend\n```"
    },
    "formal_statement": "theorem mathd_number_theory_1 (n m : \u2115) (h : n \u2264 m) : n! * n ^ (m - n) \u2264 m! :=",
    "informal_statement": "For any two natural numbers \u0027n\u0027 and \u0027m\u0027 where \u0027n\u0027 is less than or equal to \u0027m\u0027, the factorial of \u0027n\u0027 multiplied by \u0027n\u0027 raised to the power of the difference between \u0027m\u0027 and \u0027n\u0027 is less than or equal to the factorial of \u0027m\u0027.",
    "model_name": "meta-llama/Meta-Llama-3-70B-Instruct",
    "natural_language": "This statement claims that for any two natural numbers n and m, where n is less than or equal to m, the product of the factorial of n and n raised to the power of the difference between m and n is less than or equal to the factorial of m. This statement appears to be related to number theory and combinatorics, as it involves factorials and exponentiation.",
    "proof": "theorem mathd_number_theory_1 (n m : \u2115) (h : n \u2264 m) : n! * n ^ (m - n) \u2264 m! :=\nbegin\n  induction m with k hk generalizing n,\n  { cases n, { refl }, { cases h } },\n  cases n,\n  { simp, },\n  { have h\u0027 : n \u2264 k := le_of_lt (lt_of_le_of_lt h (nat.lt_succ_self k)),\n    have := hk n h\u0027,\n    rw [nat.factorial_succ, nat.factorial_succ] at this,\n    have := mul_le_mul this (pow_le_pow_of_le_left (le_refl _) (le_of_lt (nat.lt_succ_self _))),\n    simp at this,\n    assumption }\nend"
}
```

This subset can be loaded as:

```python
from datasets import load_dataset

ds = load_dataset("plaguss/test_deepseek_prover", "default")
```

Or simply as it follows, since there's only one configuration and is named `default`: 

```python
from datasets import load_dataset

ds = load_dataset("plaguss/test_deepseek_prover")
```


</details>
