miniCTX-v2 is a context-rich dataset for evaluation of neural theorem proving under a more realistic scenario. miniCTX-v2 is an updated version of miniCTX with new theorems extracted after a more recent cutoff date of November 28, 2024.

See our project page for more details.

Example Entry

An entry in the miniCTX dataset consists of the theorem statement, preceding file contents, and metadata information. For example, given the following theorem s_eq_pow_two in context:

import Mathlib.Data.Real.Basic

/-!
# Square function
We define the squaring function `s : ℝ → ℝ` to be `s x := x * x`.
-/

def s (x : ℝ) : ℝ := x * x

lemma s_eq_pow_two {x : ℝ} : s x = x ^ 2 := by
  rw [s, pow_two]

The problem is formatted in JSON as follows:

{
  # Preceding file content
  "srcContext": "import Mathlib.Data.Real.Basic\n\n/-!\n# Square function\nWe define the squaring function `s : ℝ → ℝ` to be `s x := x * x`.\n-/\n\ndef s (x : ℝ) : ℝ := x * x\n\n",
  
  # Theorem statement
  "theoremStatement": "lemma s_eq_pow_two {x : ℝ} : s x = x ^ 2",

  # Fully qualified theorem name
  "theoremName": "s_eq_pow_two",

  # Temporal metadata
  "fileCreated": {"commit":"(git commit)", "date":"(date the commit is updated)"},
  "theoremCreated": {"commit":"(git commit)", "date":"(date the commit is updated)"},

  # Source metadata
  "file": "MyProject/Square.lean",
  "module": "MyProject.Square",
  "positionMetadata": {
    # Line number the theorem is on
    "lineInFile": 10,
    # Number of tokens before the theorem
    "tokenPositionInFile": 152,
    # Number of premises (definitions, theorems) before the theorem
    "theoremPositionInFile": 1
  },

  # Dependency metadata
  "dependencyMetadata": {
    # Number of definitions or lemmas defined in this file that the theorem uses
    "inFilePremises": true,
    "numInFilePremises": 1,
    # Number of definitions or lemmas defined in this repository that the theorem uses (including in-file ones)
    "repositoryPremises": true
    "numRepositoryPremises": 1,
    # Number of total premises (in file, repository, or otherwise)
    "numPremises": 2,
  },

  # Proof metadata
  "proofMetadata": {
    "hasProof": true,
    "proof": "by\n  rw [s, pow_two]",
    "proofType": "tactic",
    "proofLengthLines": 2,
    "proofLengthTokens": 20
  }
}

Description of Each Entry

• srcContext: The context of the source file preceding the theorem, including imports and relevant definitions. This provides necessary background to understand the theorem.
• theoremStatement: The statement of the theorem being proved.
• theoremName: The name of the theorem.
• fileCreated: The git commit hash indicating when the file was created.
• theoremCreated: The git commit hash indicating when the theorem was added.
• file: The name of the file containing the theorem.
• positionMetadata:
  • lineInFile: The line number in the file where the theorem is located.
  • tokenPositionInFile: The number of tokens in the file before the theorem starts.
  • theoremPositionInFile: The number of premises (definitions, theorems) before the theorem in the file.
• dependencyMetadata:
  • inFilePremises: Indicates whether the theorem uses definitions or lemmas defined in the same file.
  • numInFilePremises: The number of definitions or lemmas from the same file that the theorem relies on.
  • repositoryPremises: Indicates whether the theorem uses definitions or lemmas defined in another file within the same repository.
  • numRepositoryPremises: The total number of definitions or lemmas from the repository (including the current file) that the theorem depends on.
  • numPremises: The total number of premises the theorem depends on, regardless of whether they are from the same file, the repository, or external sources.
• proofMetadata:
  • hasProof: Indicates whether the theorem has a proof.
  • proof: The proof of the theorem.
  • proofType: The type of proof, term proof or tactic proof.
  • proofLengthLines: The length of the proof in lines.
  • proofLengthTokens: The length of the proof in tokens.

In addition to individual entries, we also provide the link and git commit version of each split for evaluation:

• Carleson: https://github.com/fpvandoorn/carleson, commit a5d265f109105809de4aaff16776b7c16b1c0bd5
• ConNF: https://github.com/leanprover-community/con-nf, commit 51c38ad244870b8b1f40b8272b281678397dfa4f
• FLT: https://github.com/ImperialCollegeLondon/FLT, commit 4a97c893071433d0d39cbf5261d0877f864c2189
• Foundation: https://github.com/FormalizedFormalLogic/Foundation, commit 54324e6e009f0d0a288897312d3feb1c0165ad19
• HepLean: https://github.com/HEPLean/PhysLean, commit fe082d93c2775beee6634b24b34c8482a02ba8a8
• Mathlib: https://github.com/leanprover-community/mathlib4, tag v4.16.0
• Seymour: https://github.com/Ivan-Sergeyev/seymour, commit 27c0384977032b693daca8c4fcfc5cc274e1f2d6

miniCTX-v2 uses Lean version v4.16.0.

Citation

Please cite:

@article{hu2024minictx,
      title={miniCTX: Neural Theorem Proving with (Long-) Contexts},
      author={Hu, Jiewen and Zhu, Thomas and Welleck, Sean},
      journal={arXiv preprint arXiv:2408.03350},
      year={2024}
    }