Zulip Chat Archive

Stream: new members

Topic: norm_num for deciding primality?


Kevin Cheung (Sep 06 2024 at 18:50):

In the documentation https://github.com/leanprover-community/mathlib4/blob/24fce2d2db1a7ed39c8c5bdaf300d2ddfc83313f/Mathlib/Data/Nat/Prime/Defs.lean#L142-L142, there is this sentence: "If you need to prove that a particular number is prime, in any case you should not use by decide, but rather by norm_num, which is much faster."

However, I have the following and norm_num is underlined with red squiggly line saying the goal is unsolved.

import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Tactic.Normnum

example : Nat.Prime 3 := by decide

example : Nat.Prime 3 := by norm_num

Is there a more powerful version of norm_num that needs to be imported? If so, what would that be?

Kyle Miller (Sep 06 2024 at 18:53):

Import Mathlib.Tactic.Normnum.Prime, which has the norm num extension for primality.

Kevin Cheung (Sep 06 2024 at 18:53):

Thanks!

Kevin Cheung (Sep 06 2024 at 18:55):

Strange. When I perform a search for "Mathlib.Tactic.Normnum.Prime" at https://leanprover-community.github.io/mathlib4_docs/search.html?sitesearch=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib4_docs&q=mathlib.tactic.normnum.prime I got no results.

Ruben Van de Velde (Sep 06 2024 at 18:58):

It's a file

Kevin Cheung (Sep 06 2024 at 18:59):

I see. My bad.

Kyle Miller (Sep 06 2024 at 19:08):

It's worth browsing the Mathlib/Tactic/Normnum folder to see what norm num plugins are available

Kevin Cheung (Sep 06 2024 at 19:14):

Thanks for the tip.


Last updated: May 02 2025 at 03:31 UTC