Examples

OpenATP ships a handful of trivial theorem examples, each an exercise from Mathematics in Lean. These are provided primarily as a convenience for testing compute and prover setup.

Running an example

Use example_task() to load a task from the EXAMPLE enum.

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

prover = standard_prover("claude", backend=DockerBackend())
result = prover.prove(example_task(EXAMPLE.MUL_REORDER), output_dir="runs/example")

assert result.success

Available examples

MUL_REORDER

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

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

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

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

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