DeepTheorem is a mathematical reasoning dataset that aims to enhance the mathematical reasoning capabilities of Large Language Models (LLMs) through informal theorem proving based on natural language.

This dataset contains 121,000 IMO-level informal theorems and proofs, covering multiple mathematical fields. Each theorem-proof pair is strictly annotated, as follows:

• o3-mini Proofs: Proofs generated or verified by the o3-mini model ensure mathematical accuracy.
• Truth value: The truth value of the theorem extracted from the o3-mini proof, indicating whether the theorem is true or false.
• Difficulty: Categorized by complexity to suit various LLM abilities.
• Categories: Covers algebra, geometry, number theory, etc.
• Variant: A positive or negative variant of a theorem that has the same or opposite truth value as the original theorem.