The lcm of the first m numbers is at least 2^m (Lemma 3.1)
ProvedAKS.lcm_lowerLemma 3.1 of the paper: for m at least 7, the least common multiple of the numbers 1 through m is at least 2^m. This is the classical Chebyshev-type bound of Nair that the paper cites, and it is the counting ingredient of Lemma 4.3: it guarantees that the least common multiple of the window of candidate r's outruns the product that all the bad candidates divide, so that at least one candidate in the window has a large order of n.
Formalization Note The lcm is the definition lcmFirst m, the fold of Nat.lcm over the list of the first m numbers.
import Mathlib import Definitions.Def_AKS_poly import Definitions.Def_AKS_alg
namespace AKS /-! Lemma 3.1 of the paper: the lcm of the first m numbers is at least 2^m. -/ theorem lcm_lower (m : ℕ) (hm : 7 ≤ m) : 2 ^ m ≤ lcmFirst m := by sorry end AKS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every m at least 7, 2^m is at most lcmFirst m, the least common multiple of the numbers 1, ..., m.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.