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 and mathlib.

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.