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:
{
