About

Methodology.

Qnarre is the public-facing wrapper around the proving/ Lean4 + LLM-predicate kernel. The kernel never reads natural language; predicate sub-agents return Booleans with evidence quotes; Lean composes the formal proof.

Predicate uncertainty is shown but never used to gate the verdict — a low-confidence predicate is still a Boolean fact in the kernel.

Cite: Quantapix Qnarre · Lean4 kernel · 2026