Examples

The package ships a handful of tiny example tasks — each a single sorry’d exercise from Mathematics in Lean. They double as a setup smoke test: example_task() stages one into the pinned Mathlib skeleton (via create_project()) and hands you a ready-to-run ProofTask.

import tempfile

from open_atp.backends.docker import DockerBackend
from open_atp.examples import EXAMPLE, example_task
from open_atp import standard_prover

prover = standard_prover("agent:claude", backend=DockerBackend())
result = prover.prove(example_task(EXAMPLE.MUL_REORDER), tempfile.mkdtemp())
print("success:", result.success)

Pass any EXAMPLE member. The bundled exercises are:

MUL_REORDER

C02 “Calculating” — reorder a product of reals.

import Mathlib

/-! From *Mathematics in Lean*, C02 "Calculating": reorder a product of reals
using commutativity and associativity. -/

example (a b c : ℝ) : c * b * a = b * (a * c) := by
  sorry

ABS_MUL_LT

C03 “Logic” — a product of two reals, each smaller in absolute value than a small ε, is itself smaller than ε.

import Mathlib

/-! From *Mathematics in Lean*, C03 "Logic": a product of two reals each smaller
in absolute value than a small `ε` is itself smaller than `ε`. -/

theorem my_lemma : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
  sorry

INTER_SUBSET

C04 “Sets and Functions” — intersecting both sides of a subset relation with the same set preserves it.

import Mathlib

/-! From *Mathematics in Lean*, C04 "Sets and Functions": intersecting both sides
of a subset relation with the same set preserves it. -/

variable {α : Type*} (s t u : Set α)

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
  sorry

INTER_UNION_DISTRIB

C04 “Sets and Functions” — intersection distributes over union.

import Mathlib

/-! From *Mathematics in Lean*, C04 "Sets and Functions": intersection
distributes over union. -/

variable {α : Type*} (a b c : Set α)

example : a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) := by
  sorry

SMUL_ADD

C09 “Linear Algebra” — scalar multiplication distributes over vector addition in a module.

import Mathlib

/-! From *Mathematics in Lean*, C09 "Linear Algebra": scalar multiplication
distributes over vector addition in a module. -/

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (a : K) (u v : V) : a • (u + v) = a • u + a • v :=
  sorry