ReplaceNativeDecide:
Automated Verification of native_decide

You see Lean proofs in the wild containing native_decide. Some are produced by AIs, including Aristotle and Claude Opus. Now, most of these uses of native_decide are benign; they are often useful as quick ways to establish base cases. But native_decide asks you to trust the entire Lean compiler code; and there are known exploits that use native_decide and @implemented_by to prove false. Also, proofs with native_decide cannot be checked with tools that use Environment.replay, including lean4checker and SafeVerify.

What to do? If you are prompting Opus to produce a Lean proof, you can ask it to not use native_decide. If you see a Lean proof where uses of native_decide are limited to small lemmas, you can independently verify the conclusions of those lemmas.

Another approach to verification of native_decide proofs: ask an AI to replace each native_decide with a proof that does not use it. This repo contains a Claude Code subagent definition .claude/agents/replace-native-decide.md, that defines a subagent that focuses on a particular native_decide in a Lean proof, and replaces it with an explicit proof without native_decide.

I am not necessarily advocating to eliminate native_decide. That is up to you to decide. You may well decide to keep both versions, one with native_decide and one with the replacement proof. The native_decide proof may be shorter, more intuitive to read, and more efficient, while the replacement proof provides added security and peace of mind. In the long term, my preference would be for larger and larger parts of the Lean compiler to become verified, so that eventually executable code with proofs of correctness can become fully trusted.

How to use it

• Make sure the project directory has Lean and Mathlib installed. E.g. lake exe cache get. Use the newest version of Lean and Mathlib if you have a choice. If it is an externally provided proof, it will usually specify the lean and mathlib versions.
• Make sure the Lean file in question compiles without errors: lake build <filename> or lake env lean <filename>.
• The agent will be modifying the file; so make sure you have a backup copy of the file.
• Copy the file .claude/agents/replace-native-decide.md into your claude code agent directory, either ~/.claude/agents/ for user-wide agents or .claude/agents/ in the project directory for project-specific agents.
• Then start (or restart) Claude Code (claude). Use the smartest model available (currently Opus 4.5). Type /agents to confirm that the replace-native-decide subagent is installed.
• Prompt Claude to invoke the replace-native-decide subagent on the file. E.g. " contains several uses of native_decide. Invoke the replace-native-decide subagent to replace the first native_decide with an explicit proof." Or: "Invoke replace-native-decide subagent sequentially, one for each native_decide in . For subsequent invocations, you may provide the agent with suggestions on proof strategy based on what ealier agents have learned."
  • Or if you prefer headless mode: claude --dangerously-skip-permissions --model opus -p <prompt>
• For additional security, you can check the resulting proof using lean4checker or SafeVerify.
• Feel free to adapt the subagent definition to your preferred models / agentic frameworks, such as GPT / Codex CLI.

Contributions Welcome!

• Use cases where the current subagent fails, and suggestions to fix
• Recipes for particluar frequently-used Mathlib features. For example, the current subagent definition contains such a recipe for padicValNat, suggested by Mario Carneiro in a Lean Zulip thread.
• H/T Kenny Lau for suggesting decide +kernel