feat(NumberTheory): decide, #eval and norm_num for Carmichael numbers

[YaelDillies]

Provide both an efficient decidability instance and a norm_num extension to decide whether a given literal is a Carmichael number.

This lets us prove that 561 is the smallest Carmichael number "in a computationally efficient manner".

Generated by Claude Opus in several rounds of review to optimise various parts of the algorithms and make sure that the decidability instance works for both #eval and decide. I haven't made much of an effort to clean the proofs (existing proofs internal to norm_num read like garbage to me anyway).

From FormalConjectures

Assisted-by: Claude Opus 5.1

---

[github-actions]

PR summary a12253a4c6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ KorseltHelper
+ KorseltHelper.mul
+ KorseltHelper.one
+ add_two_le_of_forall_prime_dvd
+ instance : DecidablePred IsCarmichael := fun n ↦
+ isCarmichael_of_korseltHelper
+ isLeast_isCarmichael_561
+ isNat_isCarmichael
+ isNat_not_isCarmichael
+ korseltAux
+ korseltAux_eq_true_iff
+ not_isCarmichael_of_ble_two
+ not_isCarmichael_of_mod_two_eq_zero
+ not_isCarmichael_of_mul_eq
+ not_isCarmichael_of_mul_mul_eq

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit a12253a).

• +16 new declarations
• −0 removed declarations

+Mathlib.Meta.NormNum.KorseltHelper
+Mathlib.Meta.NormNum.KorseltHelper.mul
+Mathlib.Meta.NormNum.KorseltHelper.one
+Mathlib.Meta.NormNum.deriveNatPrime
+Mathlib.Meta.NormNum.evalNatIsCarmichael
+Mathlib.Meta.NormNum.isCarmichael_of_korseltHelper
+Mathlib.Meta.NormNum.isNat_isCarmichael
+Mathlib.Meta.NormNum.isNat_not_isCarmichael
+Mathlib.Meta.NormNum.not_isCarmichael_of_ble_two
+Mathlib.Meta.NormNum.not_isCarmichael_of_mod_two_eq_zero
+Mathlib.Meta.NormNum.not_isCarmichael_of_mul_eq
+Mathlib.Meta.NormNum.not_isCarmichael_of_mul_mul_eq
+Nat.instDecidablePredIsCarmichael
+Nat.isLeast_isCarmichael_561
+Nat.korseltAux
+Nat.korseltAux_eq_true_iff

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit a12253a4c6
Reference commit f61f3ed763

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[SnirBroshi]

!bench

[leanprover-radar]

Benchmark results for a12253a against f61f3ed are in. No significant results found. @SnirBroshi

• 🟥 build//instructions: +93.8G (+0.07%)

Small changes (2🟥)

• 🟥 build/module/Batteries.Data.Array.Pairwise//instructions: +25.1M (+1.23%)
• 🟥 build/module/Mathlib.NumberTheory.CarmichaelNumber//instructions: +20.9G (+207.57%) (reduced significance based on *//lines)