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.

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:

$ 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):

$ lanky check examples/l2p.py
...
proved   proved     lean         l2p.py:246  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:246  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 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'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.4.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:

pip install "lanky[lean,cas]"
git clone --branch v0.4.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, 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:

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. Checking a file again reads Lean's answers from a cache and starts no Lean, also for a question the first check ran out of time on. 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 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 (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.4.0. The core works; the edges are sharp. New in 0.4.0, the ledger says what happened where it said nothing: an oracle that raised, in a RAISED line, a claim Lean was not asked about and why, under --verbose, and a Mathlib project Lean cannot import, in the WITHOUT LEAN line; and a check after the first starts no Lean, also where the first ran out of time. Since 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. An oracle that raised over a fact is named in a RAISED line with the exception (raised in the provenance; --verbose prints where it raised), so that a crash is not read as a claim it was never offered, and --verbose says of a claim Lean's printer cannot state that Lean was not asked, and why (lean_declined). None of these 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 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:

  # 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. Each theorem is shown under a name of its own in the ledger: the facts of one owner whose parts have one name, a kernel's accesses, are told apart as Lanky.jacobi_in_bounds, Lanky.jacobi_in_bounds_2 and on.

• 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). 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().
• min and max of a variable are refused (#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). 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). 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). 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). 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), and a background process a checked file starts holds the command up until it ends (#47). Check the files of one source root per command, which runs no child process.

Install

pip install lanky

That is the 0.4.0 release, which loopty's demonstrations need (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:

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:

pip install "lanky[lean]"

Lean comes from elan, its toolchain manager (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:

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:

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. Everything it fetches stays in the project, the packed downloads (about 400 MB) included, in .lake/mathlib-cache, so deleting ~/mathlib deletes all of it; a MATHLIB_CACHE_DIR you set keeps them there instead, and the command says where they went. The first session of a process imports Mathlib, which takes seconds and about 1.5 GB of memory, and checks that it did: a project whose compiled files are damaged, by a lake exe cache get that stopped half way, say, makes the oracle unavailable, and the WITHOUT LEAN line says what Lean said and to run lake exe cache get! in the project. 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).

Lean's answers are kept in $XDG_CACHE_HOME/lanky/proofs (~/.cache/lanky/proofs by default; LANKY_LEAN_PROOF_CACHE moves it, and off turns it off), so a check after the first starts no Lean. A question the first check ran out of time on, its budget spent or an attempt timed out, is kept as where it stopped: the next check reads the same row back, with Mathlib as without it, and asks Lean again only when it is given more time, a larger budget or timeout, or has other attempts to send, such as the new case splits of a plugin's solver.

For work on lanky itself:

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: 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.
• 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.