# Lean: the divisibility-instances run

**Result:** 14 divisibility cases were checked on 2 October 2026 with
Lean 4.33.0 (toolchain `leanprover/lean4:v4.33.0`) on one side and the
Arxo package `mathlib.divisibility` with `law` 0.1.1 on the other:
10 match, 3 not comparable, 0 mismatch, 1 not checked. The Lean side ran
on the core library; mathlib statements were not executed. The mathlib
statements themselves are pinned at revision
`db584cd6d46c92f209a44c0f1c829460d327499d`, and the Arxo side anchors its
provenance to that same pin at the text level — but no mathlib file was
executed on either side in this run. The numbers belong to these versions
and to these 14 cases only.

## The task and the reference

The reference is a set of mathlib theorem statements about divisibility
and order (`dvd_trans`, `dvd_refl`, a semigroup projection, `le_trans`,
`le_of_lt`, `le_less_trans`), pinned at the revision above. The two sides
do deliberately different work with them. Lean proves each numeric
instance with its kernel: a term the kernel accepts, with the axioms
printed and inspected. Arxo applies the imported statement to the data
and returns an evaluation document with a proof graph reaching the pinned
mathlib text — the proof itself stays in the source; what Arxo certifies
is the application of an accepted result to the facts at hand. The public
pages of the two references are [Lean](https://lean-lang.org/) and
[mathlib](https://github.com/leanprover-community/mathlib4).

## What "agreement" means here

A case matches when both sides settle the same instance: Lean with an
accepted proof term, Arxo with a supporting evaluation document — or when
both sides honestly refuse it. A case is not comparable when the two
sides answer different questions by contract design: Arxo permission
facts have no counterpart in Lean, so those cases cannot meet. Pairwise
equality of proof objects is never required; what is compared is the
verdict on the instance, plus the honesty of refusals.

## Results

| Case | Instance | Lean 4.33.0 core | Arxo | Outcome |
|---|---|---|---|---|
| N-01 | transitivity with witnesses | proved (`Nat.dvd_trans` with witnesses) | TRUE_ONLY | match |
| N-02 | reflexivity at 5 | proved (`Nat.dvd_refl 5`) | TRUE_ONLY | match |
| N-03 | semigroup projection | not executed (no core analogue) | TRUE_ONLY | not checked |
| N-04 | missing premise | refusal shown by unclosed-placeholder analogue | NEITHER with reason | match as honest-refusal class |
| N-05 | missing premise | refusal shown by the same analogue | NEITHER with reason | match as honest-refusal class |
| N-06 | permission fact absent | proved as N-01 (Lean has no permission mechanism) | NEITHER with reason | not comparable by design |
| N-07 | permission fact absent | proved as N-02 (Lean has no permission mechanism) | NEITHER with reason | not comparable by design |
| N-08 | small instance by computation | proved by `decide` | TRUE_ONLY | match: both sides compute the witnesses |
| N-09 | 4 divides 6 (false) | positive goal refuted; negation proved | NEITHER with reason | match as honest-refusal class |
| N-10 | 0 divides 6 (false) | positive goal unprovable; negation proved | NEITHER with reason | match as honest-refusal class |
| N-11 | order transitivity | proved (`Nat.le_trans`), no axioms | TRUE_ONLY | match |
| N-12 | less-implies-less-or-equal | proved (`Nat.le_of_lt`), no axioms | TRUE_ONLY | match |
| N-13 | composed order step | proved by `omega` (core has no name for it) | TRUE_ONLY | match, with the naming note |
| N-14 | permission fact absent | proved as N-11 (Lean has no permission mechanism) | NEITHER with reason | not comparable by design |

Nowhere in the run is there a placeholder axiom or a native-code shortcut:
`sorry` and native decision procedures were not used, and every printed
axiom list shows core and standard axioms only.

## Where the two systems behave differently

There are no mismatches; the systematic difference is structural. Lean
has no permission mechanism, so the three permission cases (N-06, N-07,
N-14) are proved on the Lean side exactly like their unguarded twins
while Arxo answers NEITHER for the missing permission fact — by contract
design these cases are not comparable rather than decided. Refusals also
differ in form while agreeing as a class: an elaborator error on the Lean
side (N-04, N-05) and a rejected positive goal with a proved negation
(N-09, N-10) stand next to an Arxo NEITHER with a stated reason. The
contract counts the class, not the shape.

## Where the model stops

The mathlib file of the stand (`dvd_trans`, `dvd_refl`, the semigroup
projection, the order lemmas at the pinned revision) was written and its
texts were checked against the package sources, but it was never
executed: a full mathlib checkout with its build cache (about 6 to 10 GB)
did not fit the shared machine, so it was not downloaded. That is the one
recorded deviation of the run, and case N-03 carries its cost as
not checked — the projection has no core-library analogue. Beyond that:
only natural-number instances were exercised, and no timing or memory
figures were taken. Agreement on 14 instances is not a claim about either
language as a whole.

## Reproducing the run

Pin both sides: Lean toolchain `leanprover/lean4:v4.33.0` with the core
stand files (the core file must succeed; the refusals file must fail to
elaborate — that failure is the expected observation), and Arxo package
`mathlib.divisibility` with `law` 0.1.1, whose case package answers all
14 cases. Pin the text both sides point at: mathlib revision
`db584cd6d46c92f209a44c0f1c829460d327499d`. A full mathlib execution of
the stand remains a separate task for a machine with a free disk; until
then N-03 stays not checked.