HEXAGONbeta

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

A mix of human-written and AI-generated textHuman understanding: all partscs.LO — Logic in Computer Sciencecs.MS — Mathematical Software

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Nov 12, 2026 / CC BY 4.0

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.

Author comments: Published on Zenodo: https://doi.org/10.5281/zenodo.23818391

References

  1. K. Aehlig, F. Haftmann, T. Nipkow. A compiled implementation of normalisation by evaluation. J. Funct. Program. 22(1), 2012.
  2. M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry, B. Werner. A modular integration of SAT/SMT solvers to Coq through proof witnesses. CPP 2011.
  3. B. Barras. Programming and computing in HOL. TPHOLs 2000.
  4. M. Boespflug, M. Dénès, B. Grégoire. Full reduction at full throttle. CPP 2011.
  5. S. Boutin. Using reflection to build efficient and certified decision procedures. TACS 1997.
  6. A. Bove, V. Capretta. Modelling general recursion in type theory. Math. Struct. Comput. Sci. 15(4), 2005.
  7. O. Abrahamsson, M. O. Myreen. Fast, verified computation for Candle. ITP 2023.
  8. O. Caprotti, M. Oostdijk. Formal and efficient primality proofs by use of computer algebra oracles. J. Symb. Comput. 32(1--2), 2001.
  9. M. Carneiro. Lean4Lean: verifying a typechecker for Lean, in Lean. arXiv:2403.14064v3, 2025.arXiv
  10. Comparator. https://github.com/leanprover/comparator (archived; part of Lean since 4.35 as lake comparator ).link
Show all 48 referencesShow fewer references
  1. lean4checker. https://github.com/leanprover/lean4checker (archived; distributed with Lean as leanchecker since 4.28).link
  2. SafeVerify. https://github.com/GasStationManager/SafeVerify.link
  3. J. Breitner. Lean 4 pull request #14892, ``define well-founded recursion without large elimination of Acc ''. https://github.com/leanprover/lean4/pull/14892, 2026.link
  4. P. Shastri. Lean 4 pull request #9944, ``experiment: definitional well-founded recursion'' (not merged). https://github.com/leanprover/lean4/pull/9944, 2025.link
  5. J. Breitner. Lean 4 issue #5806, ``Optimizing terms for kernel reduction (meta issue)''. https://github.com/leanprover/lean4/issues/5806, 2024.link
  6. S. Wimmer, L. Noschinski. Pratt's primality certificates. Archive of Formal Proofs , 2013.
  7. L. Cruz-Filipe, M. J. H. Heule, W. A. Hunt, M. Kaufmann, P. Schneider-Kamp. Efficient certified RAT verification. CADE 2017.
  8. L. de Moura, S. Ullrich. The Lean 4 theorem prover and programming language. CADE 2021.
  9. G. Gonthier. Formal proof---the four-color theorem. Notices of the AMS 55(11), 2008.
  10. B. Grégoire, X. Leroy. A compiled implementation of strong reduction. ICFP 2002.
  11. B. Grégoire, L. Théry, B. Werner. A computational approach to Pocklington certificates in type theory. FLOPS 2006.
  12. F. Haftmann, T. Nipkow. Code generation via higher-order rewrite systems. FLOPS 2010.
  13. T. Hales et al. A formal proof of the Kepler conjecture. Forum Math. Pi 5, 2017.
  14. P. Lammich. Efficient verified (UN)SAT certificate checking. CADE 2017.
  15. lean4export. https://github.com/leanprover/lean4export.link
  16. nanoda. https://github.com/ammkrn/nanoda_lib; version 0.4.19 as distributed with the Lean 4.35 toolchain.link
  17. T. Nipkow, G. Bauer, P. Schultz. Flyspeck I: tame graphs. IJCAR 2006.
  18. V. R. Pratt. Every prime has a succinct certificate. SIAM J. Comput. 4(3), 1975.
  19. M. Sozeau, C. Mangin. Equations reloaded: high-level dependently-typed functional programming and proving in Coq. Proc. ACM Program. Lang. 3(ICFP), 2019.
  20. Y. K. Tan, M. J. H. Heule, M. O. Myreen. cake_lpr: verified propagation redundancy checking in CakeML. TACAS 2021.
  21. T. S. Tomar. A kernel-checked Lean proof that sorting networks on 13 inputs need 45 comparators. Zenodo, 2026. doi:10.5281/zenodo.23552145. Native Lean version: doi:10.5281/zenodo.23504361.DOI
  22. T. S. Tomar. A matching threshold of 2×10−32\times10^{-3} for the rotated surface code under circuit-level noise. Zenodo, 2026. doi:10.5281/zenodo.23498520. Native Lean version: doi:10.5281/zenodo.23485205; kernel-only Lean version: doi:10.5281/zenodo.23498518.DOI
  23. T. S. Tomar. Smale's sixth problem for six bodies in the plane: finiteness of central configurations for generic masses, with a proof formalized in Lean. Zenodo, 2026. doi:10.5281/zenodo.23472600. Supplement: doi:10.5281/zenodo.23472605.DOI
  24. T. S. Tomar. On the minimal dimension of range-criterion counterexamples to the PPT2^2 conjecture. Zenodo, 2026. doi:10.5281/zenodo.23651994. Lean checks: doi:10.5281/zenodo.23651991.DOI
  25. T. S. Tomar. Which fine-grained lower bounds survive the refutation of 3SUM and APSP? Zenodo, 2026. doi:10.5281/zenodo.23609699. Supplement: doi:10.5281/zenodo.23609700.DOI
  26. T. S. Tomar. The L1L^1 Poincaré constant of the Hamming cube. Zenodo, 2026. doi:10.5281/zenodo.23533350. Supplement: doi:10.5281/zenodo.23533351.DOI
  27. M. Armand, B. Grégoire, A. Spiwack, L. Théry. Extending Coq with imperative features and its application to SAT verification. ITP 2010.
  28. J. Xin, A. Schneidman, C. Cummins, K. Ram, S. Ganesh, J. Limperg. AXLE: a cloud infrastructure for Lean 4 theorem proving utilities. arXiv:2606.26442, 2026.arXiv
  29. H. Böving, S. Bhat, L. Cicolini, A. Keizer, L. Frenot, A. Mohamed, L. Stefanesco, H. Khan, J. Clune, C. Barrett, T. Grosser. Interactive bitvector reasoning using verified bit-blasting. Proc. ACM Program. Lang. 9(OOPSLA2), 2025.
  30. M. Carneiro. Mathlib.Tactic.Sat.FromLRAT (the lrat_proof command). Mathlib, 2022.
  31. S. Szeider. Streaming LRAT certificates into Lean theorems. arXiv:2607.00815, 2026.arXiv
  32. LratK, an LRAT checker evaluated by Lean's kernel (file CoveringLean/LratK.lean ). https://github.com/thiagopatzdorf/Matematica, 2026.link
  33. lean-dedep (proof of concept). https://github.com/nomeata/lean-dedep, 2026.link
  34. ReplaceNativeDecide. https://github.com/GasStationManager/ReplaceNativeDecide.link
  35. con-ron. https://github.com/leanprover/con-ron.link
  36. Mathlib pull requests #25297, ``lint against using native_decide '' (2025), and #43194 ( linter.style.native , 2026). https://github.com/leanprover-community/mathlib4/pull/25297.link
  37. J. Breitner. Lean 4 pull request #12887, ``optimize string literal equality simprocs for kernel efficiency''. https://github.com/leanprover/lean4/pull/12887, 2026.link
  38. F. Haftmann. Code generation from Isabelle/HOL theories. Isabelle documentation (tutorial codegen ).

Version history

  1. v1 · 27 pagesSubmitted by Tejasvi Singh TomarPublished on Zenodo: https://doi.org/10.5281/zenodo.23818391CurrentNov 12, 2026