examples

Tiny, ready-to-run example tasks bundled with the package — each a single sorry’d exercise from Mathematics in Lean. example_task() stages the chosen asset into the pinned Mathlib skeleton (create_project()), yielding a complete ProofTask. Handing it to prove() exercises the whole pipeline (stage → generate → verify) end to end, so it doubles as a setup smoke test. The exercise sources are shown on the Examples page.

open_atp.examples.example_task(name: EXAMPLE) → ProofTask

Stage a bundled example into a ready-to-run ProofTask.

name is an EXAMPLE member (the exercise sources are shown on the Examples page). The bare .lean asset is staged into the pinned Mathlib skeleton (create_project()) under a fresh temp directory, so the returned task is a complete lake project pinned to DEFAULT_IMAGE – hand it straight to prove().

class open_atp.examples.EXAMPLE(*values)

The bundled examples accepted by example_task().

Each member’s value is the .lean asset’s filename stem under examples/assets; all are exercises from Mathematics in Lean:

• MUL_REORDER – C02 “Calculating”: reorder a product of reals.

• ABS_MUL_LT – C03 “Logic”: a product of two small reals is small.

• INTER_SUBSET – C04 “Sets and Functions”: intersecting preserves a subset relation.

• INTER_UNION_DISTRIB – C04 “Sets and Functions”: intersection distributes over union.

• SMUL_ADD – C09 “Linear Algebra”: scalar multiplication distributes over addition.