Das Musterstück — Codex Calculemus

KERNEL-CHECKED An integration specimen, not a promulgated law. It carries no Q.E.D. and claims no discovery. What it demonstrates is the daemon's whole thesis in miniature — the model proposes, the kernel decides — so it is stamped Q.E.F., quod erat faciendum: which was to be made.

Leanstral 1.5 — Mistral's Lean prover, model id labs-leanstral-1-5 — was dropped into the Leibniz theorem daemon's prover ensemble as a kernel-checked prover with zero code changes. This is a field note on that construction: a thing that was built, and then shown to work. The one rule it answers to is the rule the whole daemon answers to.

LLMs propose; only mechanical checkers — the Lean 4.31 kernel, Z3, and exact decision procedures — decide.

No the proof looks right is ever trusted. A fast, fluent draft earns nothing for being fluent; it earns its place only when the kernel elaborates it and finds it clean.

Die Einbindung — three lines of config

Integration is not a code change. It is three environment lines. Leanstral speaks the OpenAI chat API and routes through the existing ADR-0028 per-model gateway, so no prover code moves. That is what makes labs-leanstral-1-5@mistral a first-class prover.

MISTRAL_API_KEY=<your key>
LEIBNIZ_GATEWAY_MISTRAL_URL=https://api.mistral.ai/v1/chat/completions
LEIBNIZ_PROVER_MODELS=labs-leanstral-1-5@mistral

Die Schleife — propose, then decide

The loop is the thesis rendered as code. Leanstral proposes a draft; the kernel decides whether it holds. The bar: the proof must elaborate and be axiom-clean — only Lean's canonical axioms; never sorry, never native_decide.

leanstral = prover_ensemble()[0]                 # labs-leanstral-1-5, via the Mistral gateway
kernel    = LeanReplBackend(timeout_s=180)
for src in THEOREMS:
    draft   = normalize_proof(leanstral.propose(Role.PROOF_DRAFT, src))  # Leanstral PROPOSES
    ok, why = kernel_accepts(kernel, src, draft)                          # the kernel DECIDES

Das Urteilsregister — a real run, five verdicts

Five theorems, five kernel verdicts. Three real induction proofs accepted; two rejected — one for reaching for native_decide (correct answer, wrong trust footprint), one that simply does not elaborate. Neither is trusted.

ACCEPT t1(n : Nat) : n + 0 = n

axiom-clean (propext) proof: by induction n with | zero => rfl | succ n ih => simp [ih]

ACCEPT t2(l : List Nat) : l.reverse.reverse = l

axiom-clean (propext) proof: by induction l with | nil => rfl | cons x xs ih => simp [ih]

ACCEPT t3(n : Nat) : n ≤ 2 * n

axiom-clean (propext, Classical.choice, Quot.sound) proof: an omega-based induction

REJECT t4: (2 : Nat) + 2 = 4

proof uses native_decide (trusts the compiler, not the kernel — forbidden) draft: by native_decide

REJECT t5(a b : Nat) : a + b = b + a

kernel rejected the proof (does not elaborate)

Der Kernpunkt — three real induction proofs accepted; two rejected — one for reaching for native_decide (correct answer, wrong trust footprint), one that simply does not elaborate. Neither is trusted.

Das Ensemble — N+1 consensus

No single prover promulgates a claim. A claim promulgates only when ≥ 2 distinct models each produce a kernel-verified, axiom-clean proof. Leanstral is wired ahead of DeepSeek-Prover-V2 and Goedel-Prover-V2. Different provers catch different goals — which is exactly why Leanstral belongs in the ensemble, not run alone.

A real run through the N+1 consensus cascade — one goal per row, one prover per column
goal	Leanstral	DeepSeek-V2	Goedel-V2	opus (witness)	consensus
n ≤ 2*n	✓ (lead)	✗	✗	✓	REACHED (2/2)
Even(n*(n+1))	✗	✗	✗	✓	NOT reached (1/2)

Die Reichweite — honest numbers

Graded across a 12-goal set through the real draft → repair loop. Reported plainly, blind spots included:

PASS@1 ≈ 58–66% · BEST-OF-5 ≈ 66% · ~0.7s per draft.
Genuinely proves: a ring-based induction for Even(n·(n+1)); a closed ∑_{i<n}(2i+1) = n², cleanly.
Blind spots (systematic): reproducibly botches a + b = b + a; did not one-shot hard modular goals like n(n+1)(2n+1) % 6 = 0.

Bottom line: a strong, fast one-shot Lean prover — best as one voter under kernel-checked consensus, not run alone.

Zwei Notizen vom Handwerk — two dev notes

temperature=0 → HTTP 400: {"message":"top_p must be 1 when using greedy sampling.", "code":"3054"} — greedy needs top_p=1.
Labs models are off by default; first call returned 403 labs_not_enabled — enable at admin.mistral.ai/plateforme/privacy.

Der Beschluss

The Lean kernel keeps the honesty; Leanstral brings the reach.

A fast prover you can rely on precisely because nothing rides on the model being right.

Die Quelle — the runnable proof of concept lives in the leibniz-daemon repo at examples/leanstral/: github.com/elementalcollision/leibniz-daemon → examples/leanstral ↗. Config-only integration. It currently sits on open PR #324; the link may 404 until it merges — that is fine.