[
    {
        "nl_problem": ["Prove that for any natural number n, n + 0 = n."],
        "nl_solution": [
            "Consider any natural number n.",
            "Using the properties of addition, we know that adding zero to any number does not change the value of that number.",
            "Therefore, we can conclude that n + 0 = n."
        ],
        "nl_solution_sketch": [
            "Consider any natural number n.",
            "From properties of addition, adding zero does not change its values.",
            "Thus, n + 0 = n."
        ],
        "fl_problem": ["theorem n_plus_zero_normal : ∀ n : ℕ, n + 0 = n := "],
        "fl_partial_sketch": [
            "by\n",
            "  -- We have the fact of addition n + 0 = n, use it to show left and right are equal.\n",
            "  have h_nat_add_zero: ∀ n : ℕ, n + 0 = n := <TODO_PROOF_OR_HAMMER>\n",
            "  -- Combine facts with to close goal\n",
            "  <TODO_PROOF_OR_HAMMER>\n"
        ],
        "src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"], 
        "fl_header_sketch":  [
            "import Mathlib.Data.Nat.Basic",
            "import Aesop"
        ],
        "path_2_file": "~/gold-ai-olympiad/lean_src_proj/lean_basics/basic_nats_using_mathlib_nats2_simp_no_rw.lean",
        "fl_statement_idx": "0"
    },



    {
        "nl_problem": ["Prove that for any natural number n, n + (m + 1) = (n + m) + 1."],
        "nl_solution": [
            "Consider any natural numbers n and m. We want to show that n + (m + 1) = (n + m) + 1.",
            "Using the properties of addition, we know that adding 1 to the sum of n and m is the same as first adding m to n and then adding 1.",
            "Therefore, we can conclude that n + (m + 1) = (n + m) + 1."
        ],
        "nl_solution_sketch": [
            "Consider any natural numbers n and m.",
            "From properties of addition, adding 1 to the sum of n and m is the same as first adding m to n and then adding 1.",
            "Thus, n + (m + 1) = (n + m) + 1."
        ],
        "fl_problem": ["theorem plus_n_Sm_proved_formal_sketch : ∀ n m : ℕ, n + (m + 1) = (n + m) + 1 := "],
        "fl_partial_sketch": [
            "by\n",
            "  -- We have the fact of addition n + (m + 1) = (n + m) + 1, use it to show left and right are equal.\n",
            "  have h_nat_add_succ: ∀ n m : ℕ, n + (m + 1) = (n + m) + 1 := <TODO_PROOF_OR_HAMMER>\n",
            "  -- Combine facts to close goal\n",
            "  <TODO_PROOF_OR_HAMMER>\n"
        ],
        "src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"], 
        "fl_header_sketch":  [
            "import Mathlib.Data.Nat.Basic",
            "import Aesop"
        ],
        "path_2_file": "~/gold-ai-olympiad/lean_src_proj/lean_basics/basic_nats_using_mathlib_nats2_simp_no_rw.lean",
        "fl_statement_idx": "2"
    },



    {
        "nl_problem": ["Prove that for any natural number n and m, n + m = m + n."],
        "nl_solution": [
            "Consider any natural numbers n and m. We will prove the statement by induction on n.",
            "Base case: When n = 0, we need to show that 0 + m = m + 0. By the definition of addition, we have 0 + m = m and m + 0 = m. Therefore, 0 + m = m + 0.",
            "Inductive step: Assume that for some natural number n, n + m = m + n. We need to show that (n + 1) + m = m + (n + 1).",
            "1. Start by using the fact that (n + 1) + m = n + (m + 1) and m + (n + 1) = (m + n) + 1.",
            "2. By the inductive hypothesis, we have n + m = m + n. So we can replace n + (m + 1) with (m + n) + 1.",
            "3. Now, both sides have the same structure, showing that (n + 1) + m = m + (n + 1).",
            "Thus, by induction, we have proved that for any natural numbers n and m, n + m = m + n."
        ],
        "nl_solution_sketch": [
            "Consider any natural numbers n and m. We will do induction on n.",
            "Base case: 0 + m = m + 0 by properties of addition.",
            "Inductive step, we have n + m = m + n. Then (n + 1) + m = (n + m) + 1 = (m + n) + 1 = m + (n + 1).",
            "Thus, by induction, n + m = m + n, qed."
        ],
        "fl_problem": ["theorem add_comm_proved_formal_sketch : ∀ n m : ℕ, n + m = m + n := "],
        "fl_partial_sketch": [
            "by\n",
            "  -- Consider some n and m in Nats.\n",
            "  intros n m\n",
            "  -- Perform induction on n.\n",
            "  induction n with\n",
            "  | zero =>\n",
            "    -- Base case: When n = 0, we need to show 0 + m = m + 0.\n",
            "    -- We have the fact 0 + m = m by the definition of addition.\n",
            "    have h_base: 0 + m = m := <TODO_PROOF_OR_HAMMER>\n",
            "    -- We also have the fact m + 0 = m by the definition of addition.\n",
            "    have h_symm: m + 0 = m := <TODO_PROOF_OR_HAMMER>\n",
            "    -- Combine facts to close goal\n",
            "    <TODO_PROOF_OR_HAMMER>\n",
            "  | succ n ih =>\n",
            "    -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.\n",
            "    -- By the inductive hypothesis, we have n + m = m + n.\n",
            "    have h_inductive: n + m = m + n := <TODO_PROOF_OR_HAMMER>\n",
            "    -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.\n",
            "    have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := <TODO_PROOF_OR_HAMMER>\n",
            "    -- 2. then to flip m + S n to something like S (n + m) we need to use the IH.\n",
            "    have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := <TODO_PROOF_OR_HAMMER>\n",
            "    -- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add.\n",
            "    have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := <TODO_PROOF_OR_HAMMER>\n",
            "    -- Combine facts to close goal\n",
            "    <TODO_PROOF_OR_HAMMER>\n"
        ],
        "src_header_fl_problem": ["import Mathlib.Data.Nat.Basic"], 
        "fl_header_sketch":  [
            "import Mathlib.Data.Nat.Basic",
            "import Aesop"
        ],
        "path_2_file": "~/gold-ai-olympiad/lean_src_proj/lean_basics/basic_nats_using_mathlib_nats2_simp_no_rw.lean",
        "fl_statement_idx": "3"
    }
]