Metadata-Version: 2.5
Name: lanky
Version: 0.3.0
Summary: Python for math you can check. A Lean-hosted proof language, shaped like mypy.
Project-URL: Homepage, https://github.com/xywei/lanky
Project-URL: Repository, https://github.com/xywei/lanky
Project-URL: Documentation, https://github.com/xywei/lanky/blob/main/docs/quickstart.md
Project-URL: Changelog, https://github.com/xywei/lanky/blob/main/CHANGELOG.md
Project-URL: Issues, https://github.com/xywei/lanky/issues
Author: Xiaoyu Wei
License-Expression: MIT
License-File: LICENSE
Keywords: formal-methods,lean,mathlib,proof,theorem-proving,type-checking
Classifier: Development Status :: 3 - Alpha
Classifier: Framework :: Pytest
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Quality Assurance
Classifier: Typing :: Typed
Requires-Python: >=3.12
Requires-Dist: numpy>=1.26
Requires-Dist: pymbolic>=2025.1
Provides-Extra: cas
Requires-Dist: sympy>=1.12; extra == 'cas'
Provides-Extra: lean
Requires-Dist: lean-interact>=0.11.5; extra == 'lean'
Description-Content-Type: text/markdown

# lanky

Python for math you can check.

A lanky file is ordinary Python. A claim is a function whose annotations are
its statement, in the Python an engineer already writes: sorts for the
variables, comparisons for the hypotheses, `all(... for i in Fin[n])` for a
quantifier. The bodies run. One command, `lanky check`, prints a ledger: every
claim, how strongly it is known (tested, decided or proved), who settled it,
and what it rests on.

Lean is underneath, and you write none of it. lanky reads each claim into a
term, prints the term as a Lean theorem, finds a proof, by `omega`, by an
induction whose steps sympy finds, or by a script over Mathlib's finite sums,
and has Lean check it. `--show-lean` prints the Lean for whoever asks.

```python
from lanky import theorem
from lanky.prelude import Fin, Fn, Nat


@theorem
def scan_monotone(
    n: Nat,
    cnt: Fn[Fin[n], Nat],
    off: Fn[Fin[n + 1], Nat],
    h0: off(0) == 0,
    hs: all(off(r + 1) == off(r) + cnt(r) for r in Fin[n]),
) -> all(off(a) <= off(b) for a in Fin[n + 1] for b in Fin[n + 1] if a <= b):
    """The offsets of an exclusive scan over counts are monotone."""
```

Parameters annotated with sorts are the variables, parameters annotated with
propositions are the hypotheses, and the return annotation is the goal. There is
no new syntax and no parser: lanky evaluates the annotations, and `==` inside one
builds a proposition instead of answering a bool.

Three commands:

```console
$ python examples/gauss.py           # theorems run as property tests
$ pytest examples/gauss.py           # the same theorems, collected as test items
$ lanky check examples/gauss.py      # the ledger: every claim and who decided it
STATUS  EFFECTIVE  BY             WHERE        OWNER          STATEMENT
------  ---------  -------------  -----------  -------------  -------------------------------------------------------------------------
tested  tested     property-test  gauss.py:31  gauss          n : Nat |- 2*sum(i for i in Fin(n + 1)) == n*(n + 1)
tested  tested     python         gauss.py:31  gauss          the term computes what the annotations compute
proved  tested     lean           gauss.py:39  scan_monotone  n : Nat, cnt : Fn[Fin(n), Nat], off : Fn[Fin(n + 1), Nat]
                                                              | h0: off(0) == 0
                                                              | hs: forall r in Fin(n). off(r + 1) == off(r) + cnt(r)
                                                              |- forall a in Fin(n + 1), b in Fin(n + 1) where a <= b. off(a) <= off(b)
tested  tested     python         gauss.py:39  scan_monotone  the term computes what the annotations compute

4 facts: 1 proved, 3 tested

WITHOUT MATHLIB: gauss is not proved, since only Lean with Mathlib can state it. To have Lean prove it: python -m lanky.mathlib ~/mathlib (about 7 GB), then export LANKY_LEAN_MATHLIB=~/mathlib.
```

(This run is on a machine with the `lean` extra installed, and no Mathlib,
which the last line says how to set up. CI runs it on one too, and checks
this output against what it prints.)

The third row is what the project is for: `scan_monotone` is proved by Lean.
Its statement is printed whole, a part to a line: the variables, each
hypothesis under the name of its parameter, and the goal after `|-`.
Under each claim is its reading. lanky reads an annotation by running it on
symbolic terms, and every oracle is handed the term that run builds, so a proof
is a proof of the term. To check that the term is what was written, the
annotations are run again as plain Python at drawn values and the term is
evaluated at the same values: `tested python` says they agreed at every draw.
The proof rests on that check, so the `EFFECTIVE` column says what it is worth,
`tested`. The same file, on a machine without Lean, reads `tested
property-test` and exits 0 just the same: the status column says how strongly
each fact is established, and the `EFFECTIVE` column, there only when some fact
is worth less than its status, what it is worth. A `WITHOUT LEAN` line under
the table then names the claims Lean would prove, and the command that
installs it.

**Facts rest on facts.** A fact can rest on others, and the ledger shows it
worth no more than they are. `scan_monotone`'s proof rests on its reading,
and is worth `tested`. In `examples/sumpy_recurrence.py`, sumpy's compressed
Taylor recurrence for the 2-D Laplace kernel is proved by Lean for every
order under the kernel's harmonicity, an axiom the file cites, so it reads
`proved under harmonic` and is worth `assumed` until someone proves the
axiom. And a plugin's facts rest on lanky's: in loopty's flagship, the row
that applies the same theorem to a kernel rests on the theorem's proof and on
the kernel's postcondition, which isl decided from what the kernel stores and
Lean proved again (two rows of its ledger, with Lean and Mathlib):

```text
$ lanky check examples/l2p.py
...
proved   proved     lean         l2p.py:249  reconstruct        (forall i in Fin(nb), a in Nat, b in Nat where a < 2 and a + b <= 10. R[i, a, b] == C[i, a, b])
                                                                  and (forall i in Fin(nb), a in Nat, b in Nat where a + b + 2 <= 10.
                                                                    R[i, a + 2, b] == -R[i, a, b + 2])
proved   tested     lean         l2p.py:249  reconstruct        by on_every_triangle, for every D with pde and stored:
                                                                  forall i in Fin(nb), a in Nat, b in Nat where a + b <= 10. R[i, a, b] == D[i, a, b]
...
```

The first row is `reconstruct`'s postcondition, the copies and the
recurrence, two of the theorem's hypotheses. The second is the theorem's
conclusion about the kernel's array, for every table `D` the other two hold
of, and is worth `tested` because the theorem is.

## Kernels: loopty

lanky knows nothing about arrays or loops. [loopty](https://github.com/xywei/loopty)
plugs in a theory of loop kernels, an isl oracle, a loopy executor and a
`run` verb, so that a kernel written as a typed Python function, and every
transform of it, becomes facts in the same ledger: isl decides each one,
Lean proves it again from loopty's own description of the kernel, and a
kernel cites the theorem it computes. Its five demonstrations, each written
after a kernel of a scientific code, and what lanky proves in each with
Mathlib:

| loopty demo | written after | the theorem, proved for every order or size |
|---|---|---|
| `examples/l2p.py` | sumpy's L2P for the 2-D Laplace kernel | the compressed Taylor recurrence rebuilds every derivative, applied to the kernel that rebuilds each box's triangle |
| `examples/hexahedra.py` | grudge PR #418's weak gradient and divergence | the Kronecker operator is three one-axis passes, cited by the programs, whose postconditions Lean proves from it |
| `examples/advection.py` | grudge #418's weak advection right-hand side | the inverse mass pushed inward, and the lift onto the face nodes the face gather's transpose |
| `examples/layer_potential.py` | pytential's direct QBX with sumpy's line-Taylor expansion | the line-Taylor coefficients, from the recurrence a logarithm's coefficients satisfy (which is cited), tied to the terms the single layer adds |
| `examples/assembly.py` | PyOP2's P1 mass assembly, from firedrake's tests | the rule exact on quadratics, the element's mass in closed form, as the kernel's postcondition, and the scatter keeping the total |

loopty's README has the demonstrations, their ledgers, and how each compares
with the code it was written after.

## Run it

lanky's own examples and loopty's demonstrations run on the 0.3.0 release
on PyPI. The examples are in the repository and not in the package, so clone
the release's tag for them. On Python 3.12 or later:

```sh
pip install "lanky[lean,cas]"
git clone --branch v0.3.0 https://github.com/xywei/lanky.git && cd lanky
lanky check examples/gauss.py
```

That much runs without Lean, and the ledger says what is missing, with the
command for each piece. Lean comes from
[elan](https://github.com/leanprover/elan#installation), at the version the
Lean REPL supports, and Mathlib, for claims about real numbers and finite
sums, is one command that fetches its compiled files:

```sh
elan default leanprover/lean4:v4.29.1
python -m lanky.mathlib ~/mathlib    # about 7 GB
export LANKY_LEAN_MATHLIB=~/mathlib
```

The first check with Lean builds Lean's REPL, which takes about a minute and
the network; a check after it reads Lean's answers from a cache and starts no
Lean. [Install](#install) has the rest.

## Where the limits are

- **A proof is a proof of the term lanky read.** The reading is checked by
  running the annotations at drawn points, not proved, so a proof is worth
  `tested`; [Known limits](#known-limits) says what that check can miss.
- **Some steps stay trusted**: the printer from lanky's terms to Lean, which
  is tested and not proved, and the Lean kernel.
- **The provers are strategies, not search.** Core Lean's ladder and
  `omega`, an induction whose steps are a linear combination, an exchange of
  finite sums, the total of a scatter. A claim that needs a lemma by name
  falls through to the tester, and its row says so.
- **Claims about real numbers need Mathlib**, about 7 GB on disk; without it
  they read `tested` or `assumed`. The Lean REPL runs a Lean release up to
  v4.32.0; CI uses v4.29.1.

## What nothing else does

- **One ledger for evidence of every strength.** A random-draw pass, an isl
  decision and a Lean proof are all facts in one table, each with a status, a
  decider, a provenance and a source location. Property-testing tools give you
  the first, SMT wrappers the second, proof assistants the third, and none of
  them will tell you, for one file, which is which. A fact can rest on others,
  and is worth no more than they are: a proof from a cited axiom reads
  `proved under` that axiom, and is worth what the axiom is.
- **Statements are the signature.** A theorem is a typed Python function. It
  imports, it is callable, it is collected by pytest, and it is readable by
  someone who has never seen a proof assistant.
- **A refutation is a witness, not a verdict.** `REFUTED` carries the
  counterexample, the offending point, or the pair of statement instances that
  makes an ordering wrong. So does the exception a caller sees.
- **A thin host with real plugins.** lanky knows nothing about arrays or loops,
  and never imports [loopty](https://github.com/xywei/loopty) (above): it
  finds it through entry points and asks it what it can do.
  `examples/pytential_skie.py` is a second consumer in miniature: a
  rule engine decides, under eight cited axioms, which of five integral
  representations give a boundary equation of the second kind. And
  `examples/sumpy_recurrence.py` is a third: sumpy's compressed Taylor
  wrangler for the 2-D Laplace kernel claims that its recurrence reconstructs
  every derivative, and the ledger has the claim `tested` by mpmath and
  `decided (heuristic)` by sympy through order 6, and, with Mathlib, `proved
  under harmonic` by Lean for every order and on the triangle `a + b <= p`
  of every order `p`, the kernel's harmonicity `assumed` on its citation.
  `examples/sum_factorization.py` proves, for every size, that a tensor-product operator on a hexahedron is three
  one-axis passes, as grudge applies it, and `examples/line_taylor.py` that
  the line-Taylor coefficients pytential's QBX evaluates are the series of a
  logarithm, at every order, with sumpy's own through order 6 decided beside
  them.

## Status

This is 0.3.0. The core works; the edges are sharp. New in 0.3.0, Lean checks
what a plugin's solver decides, part by part, and Mathlib mode proves claims
about finite sums, scatters and complex numbers for every size. Since 0.2.0,
each claim's reading is checked: the annotations are run again as Python at
drawn points and the term the oracles prove has to agree there, so a
misreading is refuted rather than proved, and a proof is worth `tested`, the
strength of that check.
Below is what works, what works in part and what does not work yet, and after
it, under Known limits, what the check cannot see and the open issues you are
most likely to meet, each with what to do about it: read that before you rely
on a proof. CI runs the suite on every change, without Lean on Python 3.12 and
3.13 and with Lean v4.29.1, and holds the tables on this page and in the
quickstart to what `lanky check` prints. Until 1.0 an interface a plugin uses
can change in a minor release; the CHANGELOG says when one does, and loopty
raises its floor to match.

**Works.**

- `lanky check FILE... [--json OUT] [--verbose] [--show-lean [TEXT]]`, exit code 1 on any
  refutation or vacuous claim. Each refuted fact is repeated under the table
  with its counterexample, its witness and its reason, the three standard
  provenance keys, read the same way whichever oracle or plugin refuted it; or
  with `no witness recorded` when it carries none of them. Each axiom is named
  under the table in a `CITED` line with its citation, and a fact left
  `assumed` that an oracle looked at and declined, saying why, in a
  `DECLINED` line with the reason it gave as `declined`, a standard provenance
  key too; neither changes the exit code. A statement that mentions a name
  nothing in it binds, a misspelt parameter or sort, gets one from the
  property tester, which names the name and draws nothing. Two claims with
  one fact id, which a factory gives the claims it makes since an id names a
  definition, fail the check: the first is checked and the others are named
  in a `DUPLICATE` block, unchecked, rather than one silently replacing
  another. Files from different source roots are checked in a process per
  root, so two directories that each hold a `helpers.py` are each checked
  against their own.
- `@theorem`: statement from the signature, `.statement`, `.term`, `.fact()`,
  `.test()`, `.report()`, `.lean()`; callable on concrete values.
- `@axiom(cite=...)`: a statement written like a theorem and taken on a
  citation. Its fact is `assumed (axiom)`, with the citation in its
  provenance; no oracle is asked to establish it, and the property tester
  still looks for a counterexample, so an axiom copied down wrong is refuted
  (and one whose hypotheses nothing satisfies is caught as vacuous).
- The reading of every claim is checked (#91). lanky reads an annotation by
  running its Python on symbolic terms, and the oracles are handed the term
  that run builds. Each theorem and axiom gets a second fact, of kind
  `faithful` and statement `the term computes what the annotations compute`:
  the annotations are run again as plain Python at drawn values, six draws of
  small values and domain ends, one at each integer written in the claim or
  in a helper it calls and next to it, and then 32 of the property tester's,
  the term is evaluated at the same values, and the two have to agree. The
  annotations run again in a copy of the module taken just before the claim
  was read, its tables and arrays included, so a table the module changes
  after the claim is read as it was, and each draw starts from that copy.
  Both readings read the connectives and the quantifiers three-valued, as
  lanky does, so a point where both have no answer does not keep the points
  after it from being compared. A disagreement
  refutes the reading, with the draw, the annotation as written and both
  answers, and the claim is offered to no oracle and fails the check: a hash,
  a text, `is`, an attribute or a comparison of types that answered from the
  term object, in the annotation or in a helper or a library it calls, is
  refuted at a point instead of proved. Every pass, decision and proof of a
  claim rests on its reading, so a proof is worth `tested` in the `EFFECTIVE`
  column, and `proved under faithful:name` where the reading could not be run
  at a point, with the reason in a `DECLINED` line. The pytest plugin fails a
  theorem whose reading is refuted.
- Facts rest on facts. `@theorem(uses=[...])` names the theorems, axioms or
  fact ids a theorem rests on, and a plugin sets `Fact.rests_on` on the facts
  it builds. The ledger reads the graph: a row says what it is established
  under (`tested under nicomachus`), and an `EFFECTIVE` column gives the
  weakest status over everything a fact rests on whenever that is weaker than
  its own. `--json` carries `rests_on`, `effective`, `effective_heuristic`
  and `under`. An id no fact in the ledger has counts as an assumption, and
  `lanky check` names it under the table. An id names a definition by the
  module its file's path gives it under its source root,
  `theorem:helpers.lemma@12`, and not by the name the module was imported
  under, so a theorem has the same id in its own file's ledger and in the
  `rests_on` of a file that imports it. A plugin keys its facts the same way,
  with `lanky.ledger.fact_id` and `lanky.check.module_name`.
  `examples/nicomachus.py` is the worked case.
- `@rewrite`: a transformation as a claim. A function of no arguments returns
  `(source, target)`, `obligation=` names what has to hold between them, and
  the fact reads `source ~> target (obligation)`, with a `RewriteTerm` for an
  oracle that knows the obligation to decide. A plugin builds the same shape
  with `lanky.rewrites.rewrite_fact`, and a subclass of `Rewrite` can claim
  more about its target. `examples/pytential_skie.py` is the worked case.
- Trust classes, strongest first: `kernel`, `decision-procedure`, `heuristic`,
  `test`. A decider complete for the fragment it accepts is a decision
  procedure; one that can fail to answer inside it, or whose answers are not
  guaranteed, such as a simplifier, is a `heuristic`. The table marks a fact
  one decided `decided (heuristic)`, and a counterexample the property tester
  finds overrules it. What rests on such a fact is worth `decided (heuristic)`
  at most, in the `EFFECTIVE` column and as `effective_heuristic` in the JSON.
  The oracle that settles a fact leaves its trust class in the provenance.
- The CAS oracle, `cas`, a `heuristic`, where sympy is installed (the `cas`
  extra). It decides a statement that asserts equations, alone, in a
  conjunction or under universals over numbers, with sides built from
  arithmetic, `abs`, `exp`, `log` and `sqrt`, when `sympy.simplify` takes
  the difference of the sides of every equation to `0`, and it declines
  everything else, a difference left over included, with the reason: what
  sympy cannot simplify away is no counterexample, and the property tester
  is asked next. A variable is a symbol with what its sort grants, so
  `sqrt(x**2) == abs(x)` is decided for a real `x` and declined for a
  complex one, and the hypotheses are not read. `lanky.cas` is the bridge,
  both ways, and refuses what it cannot translate faithfully: a family, a
  reduction, a floor division, a variable whose sort is not a set of
  numbers, a real `log` or `sqrt` of what sympy cannot show is not
  negative, where sympy's value is complex and Python's `math` raises.
  sympy is imported on the first fact, never with lanky; before its deadline
  the oracle reads only a statement's shape, and it translates the statement
  within it.
- The ledger: six statuses, provenance, JSON, a rendered table.
- The prelude: `Nat`, `Int`, `Real`, `Complex`, `Bool`, `Prop`, `Fin[n]`,
  `Fn[A, B]` and `Fn[A, B, C]`, a family with two indices (a matrix,
  `Fn[Fin[n], Fin[m], Real]`, which is `Fn[Fin[n], Fn[Fin[m], Real]]`),
  applied as `F[i, j]`, `F(i, j)` or `F(i)(j)`, one entry to every reading
  and to Lean, and given to a theorem called as a function as nested lists,
  an array or a function, refinement by `T & prop`, the sum
  `Fin[n] + Fin[m]` of index types (carried for plugins, not yet a binder
  domain), exactness classes;
  and `lanky.exp`, `lanky.log` and `lanky.sqrt`, which build a term from a
  term, and from a number in an annotation, so that `exp(1)` there is `e` to
  every oracle and not the float nearest it, and are `math`'s (or `cmath`'s)
  functions at a number anywhere else: in the file run as a program, and in
  a function an annotation calls. Python's `abs` of a term is lanky's `Abs`,
  so a comparison of it is a proposition.
- Property testing, including satisfying a definitional hypothesis by
  construction rather than rejection sampling, so a theorem about a scan is
  genuinely tested and not vacuously passed. A synthesized value has to land
  inside the family's codomain, so an unsatisfiable definition drops the draw
  rather than putting a point outside its sort into it. A pass over zero valid
  draws is never reported as `TESTED`: the fact stays `ASSUMED` and its
  provenance says `untested` and why. The reals are read exactly, as Lean
  reads them: `Real` and `Complex` are drawn as fractions whatever their
  exactness class, and `exp`, `log` and `sqrt` are enclosed in intervals
  where their values are not rational (`src/lanky/intervals.py`), so a claim
  is refuted only where the enclosures exclude it.
- Refusing the ways a statement can silently mean something other than what was
  written: a guard joined with Python's `or`, an `and` or `or` used as a value,
  a `not` in a guard, an `if` statement inside a function an annotation
  calls, and a symbolic guard over a concrete domain (`if n > 100` in a sum
  over `Fin[3]`), which a walk of the domain would drop; a body that is a
  term there is kept, `all` and `any` of it being the conjunction and the
  disjunction of its values at the points. The connectives are
  `&`, `|` and `~`. Only a generator's `if` clause records a guard: a
  conditional expression (`a if i < 3 else b`), a `not` in a body and a
  comparison of two tuples or lists, which compares their items, are refused
  inside a quantifier, where each used to be read as its guard. A builtin of
  Python's in an annotation is Python's at concrete arguments (`round(0.5)`
  is `0`, and `complex(-1, -0.0)` keeps its negative zero) and refused at a
  variable, naming it (`min(x, y)`), where it used to be a free name; so is
  a truth value a builtin asks for inside a quantifier (`min(i, j)`, `i in
  range(3)`), which used to be recorded as the quantifier's guard, and a
  symbolic domain `zip` or `enumerate` walks. A theorem refuses a parameter
  annotated with a builtin type, `x: int`, or naming one anywhere in its
  annotation, `f: Fn[Fin[n], float]`, and names the sort meant. A term is no
  key of a dict and no member of a set in an annotation: `{0: 1}.get(i, 0)`
  and `i in {0, 1}` are refused, where the lookup answered from the term's
  hash as if the key were absent and Lean proved what that left. Nor is a
  term text, `f"{i}"`, or a truth value, `1 if i else 0`, which answered
  the same at every value; compare it instead, `i != 0`.
- One reading of arithmetic for every oracle. `Nat` means an integer that is
  not negative, and the Lean printer says so: a natural is an `Int` with
  `0 ≤ n` as a hypothesis, and `//` and `%` are `Int.fdiv` and `Int.fmod`,
  which round the way Python's do. What Lean proves is what the property
  tester tests, so a claim is refuted, or not, whether or not Lean is
  installed: `n - 1 >= 0` over `Nat` is refuted everywhere, and `n - 1 <= n`
  is still proved where Lean is. A comparison with no variable in it, which
  only a plugin builds, is ascribed `Int` as well. A `Fraction` is a number
  like an `int`: `x ** Fraction(1, 3)` is a cube root, and not a power to the
  float nearest a third. Every declaration Lean is sent is elaborated with
  `autoImplicit` off, so a name its signature does not bind is an unknown
  identifier to Lean and never a variable Lean picks a type for.
- Vacuous claims are caught. When no draw satisfies a fact's hypotheses, the
  stronger oracles are asked whether the hypotheses alone prove `False`. If one
  does, the row reads `proved (vacuous)` and `lanky check` exits 1: the claim
  is true and says nothing, which is usually a mistake in the hypotheses. If
  none can, a warning says the hypotheses were never satisfied. A goal whose
  own guard never holds, a flipped or off-by-one generator guard, is caught
  the same way: when no draw gets through the goal quantifier's guard, the
  stronger oracles are asked whether it is empty wherever the hypotheses hold,
  and a guard empty only for some values, as `Fin[n]` is at `n = 0`, is never
  flagged.
- A statement the annotation already answered is a claim like any other:
  `-> 1 == 2` is `refuted`, `lanky check` prints why under the table, and it
  exits 1 on it.
- The Lean oracle over core Lean 4, with a tactic ladder and an induction
  strategy read off the term. No Mathlib is fetched or needed. CI runs the
  suite against Lean v4.29.1 as well as without Lean. A name Python accepts
  and Lean reserves, a variable `fun` or a theorem `scoped`, is printed
  quoted (`«fun»`). A theorem is declared as `Lanky.<name>`, so a claim
  named like a core declaration (`and_comm`, `id`, `trivial`) is not refused
  as already declared; a variable named like a root name the printer writes
  (`Int`, `Nat`, `Bool`, `Finset`) has those printed `_root_.Int` in its
  statement; and a variable named `rfl` or `_`, which `intro` and `rcases`
  read as patterns, is introduced under a fresh name. A statement that
  mentions a name nothing in it binds is declined, naming it: Lean would read
  the name as its own declaration of it, Mathlib's `round` for Python's, or
  bind it implicitly at a type of its own choosing, and prove another
  statement. An existential's conditions are conjuncts, so a disjunction
  among them is bracketed, as Python groups it. An attempt that runs
  past `LANKY_LEAN_TIMEOUT` costs that attempt alone: the REPL the driver
  killed is started again for the next. The ladder as a whole has a budget
  per fact, `LANKY_LEAN_BUDGET` (120 s), and a smaller one for the questions
  whether a fact is vacuous, `LANKY_LEAN_VACUITY_BUDGET` (30 s), which also
  leave out the attempts that cannot show `False`; the search for an
  induction's certificates counts against it, and a fact whose budget runs
  out says after how many attempts. And a REPL ends with the process
  that started it, however that process ends, a `SIGKILL` included: a small
  reaper process per lanky process kills it when the pipe from lanky
  closes, and Ctrl-C during an attempt stops it at once.
- Mathlib mode, opt-in: `LANKY_LEAN_MATHLIB` names a Lake project with
  Mathlib fetched, and `python -m lanky.mathlib DIR` sets one up from the
  project lanky ships, pinned to Mathlib v4.29.1 and every dependency at a
  commit. The oracle imports Mathlib once and prints statements over `Real`
  and `Complex` (`ℝ` and `ℂ`), sums (`∑` over `Finset.Ico`), absolute values,
  true division, floats as the rationals Python holds, and `exp`, `log` and
  `sqrt` (`Real.exp` and the rest, and `Complex.exp`, `Complex.log` and
  `Complex.sqrt`). A complex `log` or `sqrt` is Python's principal branch
  off its branch cut and not on it, so Lean proves a statement that takes
  one only after it proves that every argument stays off the cut (#59). The
  ladder goes on to `norm_num`, `positivity`, `ring`, `field_simp`,
  `linarith` and `nlinarith`, and to an induction for a sum whose bound a
  natural parameter sets, so Gauss's sum in `examples/gauss.py` reads
  `proved lean`. With the variable unset, the oracle is the core one,
  exactly.
  [docs/quickstart.md](https://github.com/xywei/lanky/blob/main/docs/quickstart.md#prove-it-with-mathlib)
  walks through it.
- Induction over families, in Mathlib mode: a claim about every order, a
  universal over naturals whose body is an equation between applications of
  the statement's families, is proved by strong induction on the order, and
  each case is closed by `linear_combination` over the hypotheses and the
  induction hypothesis, normalized by `ring`, or by `field_simp` and `ring`.
  Python finds the combination (`lanky.induction`, with sympy, the `cas`
  extra): which hypothesis to use at which point, and the multipliers, which
  may be expressions in the statement's other variables; Lean checks it.
  `lanky.oracles.lean.use_certificate` is the hook through which a plugin
  hands over multipliers of its own, and `lanky.oracles.lean.decline` leaves
  a claim to the oracles after Lean, saying why. The sumpy demonstration's
  claim for every order is proved this way, and so is its corollary on the
  triangle `a + b <= p` of every order `p`, whose recurrence holds only
  inside the order: a hypothesis is used where its guards follow from the
  bounds of the variables and from the goal's own guards, `k + b + 2 <= p`
  from the goal's `a + b <= p` at `a = k + 2`. So is a claim from an order on,
  `all(c(n) == -(-beta / alpha) ** n / n for n in Nat if n >= 1)`: the
  guard's lower bound raises the step, the orders it rules out are base
  cases `omega` closes from the guard, and a step that divides by the
  order over `ℝ` or `ℂ` shows first that the order is not zero there, which
  `field_simp` cannot see for itself.
- Exchanging finite sums, in Mathlib mode: an equation between sums,
  products of sums and quotients of a sum, under any universals, is proved
  by distributing the products into the sums (`Finset.mul_sum`,
  `Finset.sum_mul`, `Finset.sum_div`), exchanging the left side's sums one
  adjacent pair at a time until they are in the right side's order
  (`Finset.sum_comm`), and comparing the summands under all of them with
  `Finset.sum_congr` and `ring`. Python finds the order (`lanky.sums`),
  comparing the summands with sympy where it is installed; Lean checks it.
  Sum factorization, a tensor-product operator applied as three one-axis
  passes, and the Kronecker product's mixed product are proved this way for
  every size (`examples/sum_factorization.py`).
- A plugin's claims checked by Lean (`lanky.obligations`). A plugin with a
  decision procedure of its own states each claim it decides for Lean too,
  as parts, each a closed lanky term, through one method of the fact's term,
  `lean_obligation()`, with the hints its solver found: the points to take a
  universal hypothesis at, a piecewise witness for an existential goal, case
  splits. The hints carry no trust: Lean proves each part, `omega` first and
  then with the hints, and a wrong hint leaves a goal it cannot close. The
  parts are checked at once (`LANKY_LEAN_JOBS`, up to four sessions) within
  the fact's budget; a fact whose parts are all proved reads `proved lean`,
  a `LEAN` line under the table says how many of the solver's facts Lean
  proved, and how, and how many the plugin did not state for Lean, and one
  that is not proved keeps the status its solver gave it,
  with a `NOT PROVED` line naming the part and why. A refuted claim
  comes with its counterexample, and Lean proves it false there, which the
  `REFUTED` block says; a refuted fact is never turned into a proof. Lean's
  answers are kept by the hash of their source
  (`LANKY_LEAN_PROOF_CACHE`), so a file checked again is quick, and when
  every part's answer is kept, no REPL is started at all. A part about real
  numbers (`Part(..., mathlib=True)`) is stated with `ℝ` and checked where
  Mathlib is, closed by `linarith`; without Mathlib the claim is left to
  the oracles after Lean with that reason. A hypothesis that is itself a
  theorem is applied as one (`Hints.applications`): Lean is asked for
  `apply h (p := ...) (c := ...)` with the values the plugin matched, and
  checks that the theorem's conclusion is the claim. Where unknowns
  multiply, a layout's address `i + n * j` at every `n`, the plugin gives
  the steps `omega` cannot take: products not negative (`Hints.products`,
  `0 ≤ n * (m - 1 - j)` by `Int.mul_nonneg`), what Lean knows of `c // n`
  and `c % n` (`Hints.quotients`), and the arithmetic multiplied out
  (`Hints.ring`), so `omega` reads each product of unknowns as one atom;
  all in core Lean. loopty states its isl facts this way, and they read `proved lean`; it states a kernel that
  cites a theorem the same way:

  ```python
  # claim: Forall(..., conclusion, guard=theorem & postcondition)
  hints = Hints(applications=(Application(0, (("p", p), ("c", c))),))
  Part("applied", "on_the_triangle gives R == D", claim, hints, mathlib=True)
  ```
- `--show-lean` prints the Lean of every row that has some, or of the rows
  whose owner, id or statement contains the text it is given: the file that
  replays a proof, a plugin's parts as they were tried, a refutation's
  theorem. It is the one place Lean's words appear.
- Plugin discovery by entry point, and `lanky <verb>` from the registry.
- The pytest plugin.

**Partial.**

- The property tester satisfies hypotheses of the shape `f(i) == e` by
  assignment and rejection-samples everything else, so an awkward hypothesis can
  end with no valid draws. The fact is then `ASSUMED`, never falsely `TESTED`.
- Division by zero is the one place the readings part. Lean's division is
  total, so `n // 0 == 0` is a theorem there and a `ZeroDivisionError` in
  Python; the fact carries a note, the ledger says what the sampled reading
  could not do, and the exit code stays 0. See `src/lanky/semantics.py`.
- Vacuity is found by sampling first, and sampling cannot tell hypotheses that
  hold nowhere from hypotheses that hold only where it does not look
  (`n == 1000`, with naturals drawn up to five). Both get the warning until an
  oracle proves the hypotheses inconsistent; without one, a vacuous claim
  warns and does not fail the check. A statement over a sort the tester cannot
  draw, such as a family over `Nat`, gets no warning, because no draw reached
  its hypotheses. A goal's guard is read the same way, and only the goal's
  outermost quantifier is: a guard nested deeper in the goal is not examined.
  That holds for a theorem with no parameters as well, whose goal is a goal
  and has no hypotheses to be mistaken for.
- Python's `and` between two propositions in a generator's `if` clause happens
  to produce the conjunction that was written, because of how CPython compiles
  a comprehension filter, so it is not refused. It cannot be told apart from
  two `if` clauses in the bytecode. Write `&`.
- The Lean induction strategy is a shape matcher, not proof search. A statement
  needing a different induction or a lemma falls through to the tester;
  `lanky.oracles.lean.use_tactic` pins a script by hand. The induction over
  families searches, but only for a linear combination: a step that needs a
  hypothesis used other than as an equation to combine, an inequality, or an
  instance whose guards are not linear arithmetic over the integers is not
  found, nor is a base case that holds only because the goal's own guard
  excludes it, unless that guard is a lower bound on the order by a number
  (`n >= 1`): one by another variable, or by anything else, leaves its base
  cases with no equation to combine. A function Mathlib does not have, a
  Bessel or Hankel function, has no form yet in which its recurrence is
  declared and a proof rests on it (#82).
- The exchange of finite sums reads a sum over a `Fin` with no `if`, whose
  bound mentions no other sum's binder: a filtered sum, a triangle
  (`for i in Fin[n] for j in Fin[i]`, whose sums `Finset.sum_comm` does not
  exchange) and a sum inside anything but a product, a quotient's numerator or
  another sum are left to the rest of the ladder, and so is a side with more
  than six sums. The order of the sums after distributing is the one Lean's
  `simp` was seen to leave, the right factor's sums outside the left's; a
  `simp` that leaves another costs the attempt, not a wrong proof (#128).
- The Lean printer covers core Lean: `Sum`, `Abs`, `Real`, true division and
  an exponent that could be negative raise rather than emit source Lean would
  reject. In Mathlib mode all but the last are printed, and what is still
  declined is a sum over `Nat`, a `Fin` with a real bound, a floor division or
  a remainder of a real, an order between complex numbers, and a complex
  logarithm or square root that Lean cannot show stays off its branch cut:
  each would be printed with a meaning Python does not give it. Showing that
  takes the hypotheses and guards around the argument and two cheap attempts,
  so `exp(log(z)) == z` for a nonzero `z`, true on both sides of the cut, is
  declined all the same.
- Over `Real` and `Complex` the tester's enclosures decide less than Lean
  does. Two enclosures can never show two transcendental numbers equal, so an
  equality counts as holding where the statement asserts it and its two sides
  agree to 64 bits: `exp(x + y) == exp(x) * exp(y)` is `tested`, as a
  sampled universal is, on evidence. Under a negation, in a hypothesis, or as
  a value, the same agreement decides nothing, and neither does an order whose
  enclosures overlap, such as `exp(x) * exp(-x) <= 1` at any `x` but `0`.
  Its pass rests on the draws at `x = 0` alone, and says so: the row
  reads `tested`, and a `WARNING` under the table says that the pass rests on
  thin evidence. A complex `log` and `sqrt` are Python's principal branches,
  enclosed off their branch cut, the non-positive real axis, where Python
  picks a side by the sign of a zero, which an exact number does not have.
  On the cut, and at an `exp` of an argument past `2**14`, the draw
  is left undecided. A negative number to a power that is not an integer is
  Python's complex principal value, enclosed part by part, so
  `(x ** 3) ** Fraction(1, 3) == x` is refuted at `x = -1`.
  Where Lean is total and Python raises (a division by zero, the logarithm of
  zero, the square root of a negative number), the fact carries a note in
  Mathlib mode, as an integer division by zero does in either mode.
- A family prints as a total function, so every application of one has to be
  shown in bounds before the statement can go to Lean. The check is affine
  arithmetic over the enclosing binders, not a solver, so an argument it cannot
  settle is declined rather than assumed: the statement falls through to the
  tester, which is a proof fewer and never a proof too many.
- Sampling quantifiers over `Nat` draws a handful of points. That is evidence of
  the weakest kind and the ledger says so. A sampled quantifier can be refuted
  but never confirmed: a `forall` that a draw breaks is really false, and an
  `any` that a draw witnesses really true, but an `any` that no draw witnesses
  is undecided, not false, and a `forall` that holds at every draw counts as
  evidence only where the statement asserts it. Under `~`, in a hypothesis or
  the guard of an `all`, and inside a sum or a comparison it is undecided, and
  so is a `forall` whose guard or refinement no draw passes, and a sum over
  draws of `Nat`. The tester declines such a draw and, when no draw decides the
  statement, the fact stays `ASSUMED` with the reason. A declined draw is
  replaced by another, so a pass counts only the draws it could decide; when
  those are outnumbered by the declined ones, or take fewer than three
  distinct assignments when the draws, decided or not, took more, the pass
  stays `tested` and gets a `reason`, printed under the table as a
  `WARNING`. Over `Fin` the domain is enumerated and both answers hold. The
  connectives are three-valued: an operand the draws leave open does not
  decide `&` or `|`, and a false conjunct or a true disjunct settles it
  however the operands are ordered. So are the quantifiers, an `all` being
  the conjunction of its points and an `any` their disjunction: a point the
  draws leave open, or whose guard has no answer, does not end the walk, and
  `all(p(i) for i in Fin[2])` reads as `p(0) & p(1)` does. A refinement is
  read as the hypothesis it is, so one that quantifies over `Nat` rejects a
  draw that breaks it and leaves one it held at undecided. A quantifier over a
  refined domain `T & p`, which a plugin building terms by hand can write,
  ranges over the points of `T` where `p` holds, as the Lean printer reads it:
  enumerated when `T` is, filtered draws when it is sampled.

**Not yet.**

- `CERTIFIED`. The Lean source and the tactic script are in provenance; nothing
  replays them under a checker yet.
- Real analysis beyond what the ladder finds: Mathlib mode states it, and the
  ladder is a fixed set of tactics, not proof search, so a statement that needs
  a lemma by name falls through to the tester (`use_tactic` pins a script).
- A proof scripting surface: today a proof is a tactic ladder lanky drives, not a
  Python program over a live goal.

## Known limits

An annotation is traced Python: lanky runs it on symbolic terms, and the claim
the oracles are handed is the term that run builds. Python that answers from
the term object instead of through its overloads, `is`, an attribute, or a
hash or a truth value asked for inside a helper, gives the same answer at every
value, and the term then says something other than what was written. lanky
refuses the cases it can see while it reads, and checks the rest by their
results: each claim's `faithful` fact runs the annotations again as plain
Python at about forty drawn points, in a copy of the module taken just before
the claim was read, and the term has to compute the same at each. A
disagreement refutes the reading, and no oracle is asked about the claim.

The check is sampled, as the property tester is: small values and a domain's
ends, each integer the claim or a helper it calls writes and its neighbours,
and 32 of the tester's draws. A misreading only at a point none of them
reaches is not seen, which is why a proof is worth `tested` in the `EFFECTIVE`
column. It runs your helpers at every draw: a change they make to the
module's data is made to the copy, but a side effect outside the module, a
file written or a line printed, happens at every draw. And a claim it cannot
run at a point keeps an `assumed` reading, so a proof of it reads `proved
under faithful:name`, with the reason in a `DECLINED` line: a variable of a
sort no value can be drawn of, an annotation Python evaluated when the
function was defined (add `from __future__ import annotations`), or what the
copy cannot hold as it was, such as an instance of a class of yours.

The open issues you are most likely to meet:

- **Calling a theorem does not check its reading**
  ([#96](https://github.com/xywei/lanky/issues/96)). `gauss(n=4)`,
  `gauss.report()` and `gauss.test()`, and so `python examples/gauss.py`,
  evaluate the term, even where the reading is refuted. Use `lanky check` or
  `pytest`, which make the check, or call `gauss.faithful_fact()`.
- **`math.floor` of a variable fails while the file is read**
  ([#112](https://github.com/xywei/lanky/issues/112)).
  `math.floor(x) >= x - 1` raises pymbolic's `UnknownVariableError: x`, and
  `lanky check` reports a file that does not import; so does any `math`
  function of a variable, since it asks the term for a float. Write the floor
  as a term, `x // 1`, and use `lanky.exp`, `lanky.log` and `lanky.sqrt` for
  those three.
- **`min` and `max` of a variable are refused**
  ([#66](https://github.com/xywei/lanky/issues/66)), with a `TypeError` that
  names the call. State the claim once per case: under a hypothesis `x <= y`,
  with `x` written for `min(x, y)`, and under `y < x`, with `y`.
- **A claim about a family over `Nat` is not tested**
  ([#98](https://github.com/xywei/lanky/issues/98)). The property tester
  cannot tabulate `Fn[Nat, Nat]`, so without Lean such a claim reads
  `assumed`, and `pytest` skips it. Give the family a bounded domain with a
  size parameter, `n: Nat, a: Fn[Fin[n + 1], Nat]`, and it is drawn.
- **A long step in C, or in a library, holds the check up**
  ([#108](https://github.com/xywei/lanky/issues/108)). Each draw has five
  seconds, and a function of yours is stopped at its next call or turn of a
  loop once they are spent. One step Python takes in C, `sum(range(10 ** n))`
  or `2 ** 2 ** n` inside a helper, and a library's own code are not: they run
  to their end. Keep such work out of the helpers a claim calls, or cheap at
  the values drawn, which include each integer the claim writes.
- **An installed package's state is read as it is at the check**
  ([#104](https://github.com/xywei/lanky/issues/104)). The copy holds your
  modules, the claim's and those under its source root. A helper from an
  installed package, one installed editable from elsewhere included, reads
  its package's tables as they are when the check runs, and so does code that
  reaches a module through `sys.modules` or `importlib`, so a table changed
  after the claim can hide a misreading. Keep the data a claim's helpers read
  in a module beside the claim.
- **After a helper's operation with no value, the rest of that annotation is
  not compared at that draw**
  ([#107](https://github.com/xywei/lanky/issues/107)). Where both readings
  have no value, the draw is read again with Lean's values for Python's
  errors, `x // 0` as `0` and so on, but only for the operators the annotation
  itself writes: a helper's own `1 // 0`, or an overflow anywhere, still ends
  the comparison there. Write such an operation in the annotation rather than
  in a helper.
- **On Windows, which CI does not run, a check of several source roots can
  leave processes behind.** `lanky check` runs one child process per source
  root. On Windows a child is not stopped when the command is killed, an
  interrupted child leaves its Lean REPL running
  ([#48](https://github.com/xywei/lanky/issues/48)), and a background process
  a checked file starts holds the command up until it ends
  ([#47](https://github.com/xywei/lanky/issues/47)). Check the files of one
  source root per command, which runs no child process.

## Install

```sh
pip install lanky
```

That is the 0.3.0 release, which loopty's demonstrations need
([Run it](#run-it)). lanky needs Python 3.12 or later. In a uv project, `uv add lanky`, and the
same for the extras below. The examples and the quickstart are in the
repository and not in the package; clone it to follow them.

The CAS oracle is an extra, which installs sympy:

```sh
pip install "lanky[cas]"
```

Where sympy imports, the oracle is on: an identity sympy simplifies reads
`decided (heuristic)  cas` rather than `tested  property-test`.
`LANKY_CAS_DISABLE=1` turns it off, and `LANKY_CAS_TIMEOUT` caps the seconds
sympy may take over one fact (60), translating the statement and simplifying
it.

The Lean oracle is an extra, because it pulls a sizable dependency tree and needs
a Lean toolchain on `PATH`:

```sh
pip install "lanky[lean]"
```

Lean comes from elan, its toolchain manager
([installation](https://github.com/leanprover/elan#installation)).
The toolchain the oracle runs on has to be one the Lean REPL has a build for.
With lean-interact 0.11.5 that is a Lean release up to v4.32.0 (or
v4.33.0-rc1), which elan's current `stable` is not. Given a newer `lean`, the
oracle tries each other toolchain elan has installed, newest first, and then
the newest version the REPL has, which elan downloads when the REPL is first
built. CI uses v4.29.1:

```sh
elan toolchain install leanprover/lean4:v4.29.1
elan default leanprover/lean4:v4.29.1
```

Mathlib mode needs the same extra and toolchain, and a Lake project with
Mathlib fetched, about 7 GB on disk. lanky ships the project, pinned, and one
command writes it and fetches Mathlib:

```sh
python -m lanky.mathlib ~/mathlib    # writes the pinned project, runs `lake exe cache get`
export LANKY_LEAN_MATHLIB=~/mathlib
```

The command never builds Mathlib from source; it fetches the compiled files
Mathlib publishes, keeping the packed downloads in `MATHLIB_CACHE_DIR`
(default `~/.cache/mathlib`). The first session of a process imports Mathlib, which takes
seconds and about 1.5 GB of memory. The induction over families finds its
combinations with sympy, so a claim for every order wants both extras,
`pip install "lanky[lean,cas]"`.

Without the extra, every Lean test skips with a one-line reason and the weaker
oracles do the work. `lanky check --verbose` prints each oracle and whether it
is available. The first use builds a Lean REPL, which takes about a minute and
the network, and caches it in `$XDG_CACHE_HOME/lanky/lean-repl`
(`~/.cache/lanky` by default), outside the virtual environment so that a
reinstall does not throw it away. Useful environment variables:
`LANKY_LEAN_DISABLE=1` makes the oracle a declared no-op, and the check prints
what a machine without Lean prints (the main CI job sets it),
`LANKY_LEAN_VERSION` pins a toolchain and skips the probe,
`LANKY_LEAN_CACHE_DIR` moves the cache, `LANKY_LEAN_TIMEOUT` caps each
tactic attempt (60 s), `LANKY_LEAN_BUDGET` the whole ladder of one fact
(120 s) and `LANKY_LEAN_VACUITY_BUDGET` that of a question whether a fact
is vacuous (30 s), `0` for no budget, `LANKY_LEAN_MATHLIB` turns Mathlib
mode on, and `LANKY_LEAN_MATHLIB_IMPORT_TIMEOUT` caps the Mathlib import
(600 s).

For work on lanky itself:

```sh
uv sync --group dev --extra lean --extra cas
uv run pytest -q
uv run ruff check .
```

The suite runs with the CAS oracle off, as it runs without Mathlib, and turns
it on in the tests that are about it, which skip without sympy.
`tests/test_sumpy_recurrence.py` skips without sumpy, which no extra
installs: `uv pip install sumpy` puts it in the environment.

CI runs the suite twice. The main job, on Python 3.12 and 3.13, installs no
Lean and sets `LANKY_LEAN_DISABLE=1`, so it sees what a user without the
extras sees. The job named `test with Lean` installs elan, Lean v4.29.1, the
`lean` and `cas` extras and sumpy, caches the toolchain and the built REPL
between runs, and runs the same suite with the Lean oracle on and
`LANKY_LEAN_TEST_REQUIRED=1`, under which a Lean test that cannot get a Lean
session fails instead of skipping. It then runs
`lanky check examples/gauss.py` and checks that the `proved lean` row at the top
of this page is a row the check printed. The suite compares the rest of that
table, and the quickstart's, with the real output in both jobs, reading the
row as `tested property-test` in the main one.

A third job, `test with Lean and Mathlib`, is optional: it may fail without
failing the run, since it depends on fetching Mathlib from outside GitHub. It
sets up the pinned project with `python -m lanky.mathlib`, caching Mathlib's
compiled files between runs, installs sumpy, runs `tests/test_mathlib.py`
and `tests/test_sumpy_recurrence.py` with the project required, and checks
that `lanky check examples/gauss.py` proves both rows and that the sumpy
demonstration's claim for every order is `proved under harmonic`.
The suite otherwise runs in core-Lean mode wherever it runs: it takes
`LANKY_LEAN_MATHLIB` out of its environment and hands it to the Mathlib tests
alone.

A file that carries statements needs `from __future__ import annotations` and a
ruff `F821` per-file ignore, because a size such as `n` is a symbolic variable
lanky invents while evaluating the annotation and has no binding a static checker
can see.

## Architecture

Four ideas, and everything else is one of them.

**Terms.** pymbolic is the expression language, the same one loopy uses, so a
statement and a generated kernel cannot drift apart in translation. lanky adds
`Forall`, `Exists`, `Sum`, `Abs` and `Elementary` (`exp`, `log`, `sqrt`) as
pymbolic subclasses, and comparison operators on them build propositions. The
property tester evaluates them in an exact reading of the reals, rationals and
interval enclosures (`lanky.intervals`), and the file run as a program
evaluates them as Python does.

**Facts and the ledger.** A `Fact` is a statement, a term, a status, a decider,
a provenance, a source location, and the ids of the facts it rests on. `Status`
is `tested, decided, proved, certified, assumed, refuted`. The ledger is the
output of a check and the thing a reviewer reads; it reads the facts' graph as
well, so a fact's status is shown with the assumptions it rests on and what it
is worth given them.

**Four plugin interfaces.** *Theories* turn decorated objects into facts.
*Oracles* establish facts and report a trust class. *Executors* run a decorated
object. *Verbs* are CLI subcommands. Each is an entry-point group:
`lanky.theories`, `lanky.oracles`, `lanky.executors`, `lanky.verbs`.

**Oracles strongest first.** Each plugin is installed once per name, so a
theory that arrives both in process and through an entry point does its work
once. Trust classes are ordered `kernel` (Lean) >
`decision-procedure` (isl) > `heuristic` (a simplifier: sympy, the `cas`
oracle) > `test` (property test). Each oracle answers
`can_establish(fact)`; `check_path` offers each fact to the strongest one that
says yes and stops at the first answer. A fact nobody establishes is `ASSUMED`,
which is not a failure. An oracle that cannot answer declines, so a timeout is
never read as a counterexample. One that took a fact and found it outside what
it decides returns it unchanged with the reason as `declined`, and `lanky
check` prints that under the table for a fact that stays `ASSUMED`.

Decorators are inert and registering: `@theorem` returns a callable object that
runs natively and puts itself in the registry. `lanky check FILE` imports the
file and reads the registry, keeping the claims defined in that file and none
from the modules it imports; `lanky check a.py b.py` checks both, each for its
own. A process imports a module of one name once, so files whose source roots
differ (the directories a check puts on `sys.path`: the file's own, and the one
its package is found from) are checked in child processes, one per root, while
files that share their roots share a process as they always did. A child runs
with the command's interpreter options (`-O`, `-W`, `-X`). On Linux and macOS
it is also sent `SIGTERM` when the command ends, however it ends, and kills
the Lean REPLs it started before it goes; and once it has exited, what it
wrote is copied and nothing a checked file left running holds the command up.
`check_path`, the function
underneath, imports into the process that calls it. No environment variable
changes what the code means.

## Name

- "Lean Annotations Natively Kernel-check Your math".
- LANK + y, where LANK = Lean Annotations, Native Kernel, and *lank* means long
  and thin, next to *lean*.

## Documentation

- [docs/quickstart.md](https://github.com/xywei/lanky/blob/main/docs/quickstart.md):
  the worked file, end to end, with the output the commands actually print,
  a second one with an axiom, the pytential demonstration, where a rule engine
  checks a derivation under the axioms it rests on, and the sumpy
  demonstration, where a recurrence is tested by mpmath and decided by sympy
  through an order, and proved by Lean with Mathlib for every order.
- [CHANGELOG.md](https://github.com/xywei/lanky/blob/main/CHANGELOG.md).
- [loopty](https://github.com/xywei/loopty): the sister project and lanky's
  first plugin: a typed polyhedral layer over loopy, where the facts are about
  loop kernels and isl decides them.

## AI disclosure

This project is developed with substantial assistance from AI coding agents
(Anthropic's Claude, via Claude Code). Design, direction, and review are by Xiaoyu
Wei. Generated text and code are reviewed before release, but readers should assume
AI involvement throughout.

## License

MIT. See [LICENSE](https://github.com/xywei/lanky/blob/main/LICENSE).
