TejasviTomar
October 2026 · Preprint

Re-proving native_decide facts in Lean's kernel: a study of 16 public packages and a converter

Tejasvi Singh Tomar

Abstract

Lean's native_decide proves a decidable proposition by running compiled code and records the result as an axiom. Mathlib forbids such axioms, and lake check and Comparator in Lean 4.35 reject them, as do the independent proof checkers. NativeTrust re-proves the recorded facts in Lean's kernel, with only the standard axioms and without editing the projects that contain them. Where a definition blocks kernel evaluation and NativeTrust has a version proved equal to it (for example, a fuel-indexed form of well-founded recursion), the converter evaluates a copy that uses that version. It then proves the copy equal to the original, usually by congruence. With its default settings it converts 98.2% of 52,821 native facts in 16 public packages. The three largest packages hold 94% of these facts; outside them it converts 68.5%. Nearly every converted fact needed nothing beyond plain kernel evaluation. Two tools remove the native axioms that the kernel can prove within a budget: a single import that makes each call of the tactic try the kernel first, and a source rewriter.

In plain words

Proof assistants such as Lean check proofs with a trusted core. A popular shortcut lets Lean accept a fact by running compiled code instead, which means trusting the compiler as well. Lean's main mathematics library bans the shortcut. The tool in this paper takes facts accepted through the shortcut and re-proves them with the trusted core alone, without changing the projects that use them. In ten of sixteen public projects, it succeeds for at least 95 of every 100 such facts. The ten include Amazon's proofs about Cedar, the company's language for access permissions.

Horizontal bar chart of 16 packages, sorted by share, each bar on a light grey track from 0 to 100%. cvc5/logos, lido-srv3 and cedar-spec are at 100%, TrainVerify at 99.99%, Humanfia IChO 2026 at 99.9%, asi-stack-book at 99.7%, rs-mca at 99.1%, sounio at 98.7%, formal-conjectures at 98.1% and longfellow-zk at 95.1%; Strata is at 23.1%, clean at 14.2%, BerryEsseen at 0.9%, and aks, sorting-network and aeneas at 0%. A column on the right gives each package's number of native facts, from 45,720 for TrainVerify to 1 for aeneas.
Illustration of the paper's Table 1: for each of the 16 packages, a bar shows the share of the package's native facts re-proved in Lean's kernel by NativeTrust with its default settings; the number on the right is how many native facts the package has. In 10 packages the share is 95% or more. The three largest packages hold 94% of the 52,821 native facts; 68.5% of the facts in the other 13 packages are re-proved.