AlphaProof 是用于进行数学证明的人工智能，其中，对于 IMO 2024 中的6道题中的 4 道。本系列博文，就 AlphaProof 对于 IMO 2024 P1 给出的答案进行详细讲述。这里是此系列的第一篇。

IMO 2024 P1

        题目如下：

IMO 2024 P1 答案

        α 为 偶整数 （Even Interger）。

P1问题与答案在LEAN 中的形式化（Formalization）

        如上图，IMO 2024 P1 在 LEAN 的定义，其中，表达了，两集合的相等。即 对于所有的实数α，使得，对于任一正整数（大于0的自然数）n，有 对于 i ∈ [0, n]，所有 i *  α 的 floor 值之和 是 正整数 n 的倍数。与 所有偶整数的集合 相等。

        这里， {(α : ℝ) | P α } 是集合定义的一种语法。

        等号前边的 P 是

∀ (n : ℕ), 0 < n → (n : ℤ) ∣ (∑ i in Finset.Icc 1 n, ⌊ i * α ⌋ )

        等号右边的 P 是

 ∃ k : ℤ, Even k ∧ α = k

        意思是，被定义集合的元素来自于实数集ℝ中，满足谓词命题（Predicate）P，的所有元素。

        这样，能明确，在LEAN中，IMO 2024 问题一 是如何定义的。后面的 := 符号，引出该两集合相等的证明。 而 by 关键字 引出了 使用 LEAN 中的 Tactic 机制进行证明。

        后续，本系列博文会对该证明过程，代码分析，进行尽可能清晰的讲解，希望大家关注。下面就列出，具体的证明代码，如下：

theorem imo_2024_p1 :{(α : ℝ) | (∀ (n : ℕ), 0 < n → (n : ℤ) ∣ (∑ i in Finset.Icc 1 n, ⌊i * α⌋))}= {α : ℝ | ∃ k : ℤ, Even k ∧ α = k}:= byrw [(Set.Subset.antisymm_iff ), (Set.subset_def), ]/- We introduce a variable that will be usedin the second part of the proof (the hard direction),namely the integer `l` such that `2l = ⌊α⌋ + ⌊2α⌋`(this comes from the given divisibility condition with `n = 2`). -/exists λx L=>(L 2 two_pos).rec λl Y=>?_use λy . x=>y.rec λS p=>?_· /- We start by showing that every `α` of the form `2k` works.In this case, the sum simplifies to `kn(n+1)`),which is clearly divisible by `n`. -/simp_all[λL:ℕ=>(by norm_num[Int.floor_eq_iff]:⌊(L:ℝ)*S⌋=L* S )]rw[p.2,Int.dvd_iff_emod_eq_zero,Nat.lt_iff_add_one_le,<-Finset.sum_mul,←Nat.cast_sum, S.even_iff, ←Nat.Ico_succ_right,@ .((( Finset.sum_Ico_eq_sum_range))),Finset.sum_add_distrib ]at*simp_all[Finset.sum_range_id]exact dvd_trans ⟨2+((_:ℕ)-1),by linarith[((‹ℕ›:Int)*(‹Nat›-1)).ediv_mul_cancel$ Int.prime_two.dvd_mul.2<|by ·omega]⟩ ↑↑(mul_dvd_mul_left @_ (p))/- Now let's prove the converse, i.e. that every `α` in the LHSis an even integer. We claim for all such `α` and `n ∈ ℕ`, we have`⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋)`. -/suffices : ∀ (n : ℕ),⌊(n+1)*x⌋ =⌊ x⌋+2 * ↑ (n : ℕ) * (l-(⌊(x)⌋))· /- Let's assume for now that the claim is true,and see how this is enough to finish our proof. -/zify[mul_comm,Int.floor_eq_iff] at this-- We'll show that `α = 2(l-⌊α⌋)`, which is obviously even.use(l-⌊x⌋)*2norm_num-- To do so, it suffices to show `α ≤ 2(l-⌊α⌋)` and `α ≥ 2(l-⌊α⌋)`.apply@le_antisymm/- To prove the first inequality, notice that if `α > 2(l-⌊α⌋)` thenthere exists an integer `N > 0` such that `N ≥ 1/(α - 2(l -⌊α⌋))`.By our assumed claim (with `n = N`), we have`⌊α⌋ + 2(l-⌊α⌋)N + 1 > (N+1)α`, i.e.`⌊α⌋ + (2(l-⌊α⌋) - α)N + 1 > α`,and this implies `⌊α⌋ > α`; contradiction. -/use not_lt.1 (by cases exists_nat_ge (1/(x-_)) with|_ N =>nlinarith[ one_div_mul_cancel $ sub_ne_zero.2 ·.ne',9,Int.floor_le x, this N])/- Similarly, if `α < 2(l-⌊α⌋)` then we can find a positive natural `N`such that `N ≥ 1/(2(l-⌊α⌋) - α)`.By our claim (with `n = N`), we have`(N+1)α ≥ ⌊α⌋ + 2(l-⌊α⌋)N`, i.e.`α ≥ ⌊α⌋ + (2(l-⌊α⌋) - α)N`,and this implies `a ≥ ⌊α⌋ + 1`; contradiction. -/use not_lt.1 (by cases exists_nat_ge (1/_:ℝ)with|_ A=>nlinarith[Int.lt_floor_add_one x,one_div_mul_cancel$ sub_ne_zero.2 ·.ne',this A])/- Now all that's left to do is to prove our claim`⌊(n + 1)α⌋ = ⌊α⌋ + 2n(l - ⌊α⌋)`. -/intro-- We argue by strong induction on `n`.induction‹_› using@Nat.strongInductionOn-- By our hypothesis on `α`, we know that `(n+1) | ∑_{i=1}^(n+1) ⌊iα⌋`specialize L$ ‹_›+1simp_all[add_comm,mul_assoc,Int.floor_eq_iff,<-Nat.Ico_succ_right, add_mul,(Finset.range_succ), Finset.sum_Ico_eq_sum_range]revert‹ℕ›/- Thus, there exists `c` such that`(n+1)*c = ∑_{i=1}^{n+1} ⌊iα⌋ = ⌊nα+α⌋ + ∑_{i=1}^n ⌊iα⌋`. -/rintro A B@csimp_all[ Finset.mem_range.mp _,←eq_sub_iff_add_eq',Int.floor_eq_iff]/- By the inductive hypothesis,`∑_{i=0}^{n-1}, ⌊α+iα⌋ = ∑_{i=0}^{n-1}, ⌊α⌋+2*i*(l-⌊α⌋)`. -/suffices:∑d in .range A,⌊x+d*x⌋=∑Q in .range A,(⌊x⌋+2*(Q * (l-.floor x)))· suffices:∑d in ( .range A),(((d)):ℤ) =A * ( A-1)/2· have:(A : ℤ) * (A-1)%2=0· cases@Int.emod_two_eq A with|_ B=>norm_num[B,Int.sub_emod,Int.mul_emod]norm_num at*norm_num[ Finset.sum_add_distrib,<-Finset.sum_mul, ←Finset.mul_sum _ _] at*rw[eq_sub_iff_add_eq]at*/- Combined with`∑_{i=0}^{n-1},⌊iα+α⌋ = (n+1)c - ⌊nα+α⌋`,we have `⌊nα+α⌋ = (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋)`, so`⌊nα+α⌋ ≥ (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋)`and`⌊nα+α⌋ < (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋) + 1`.Also, since `2*l = ⌊α⌋ + ⌊2α⌋`, we have`2α+⌊α⌋-1 < 2*l ≤ 2α+⌊α⌋.`-/zify[←mul_assoc, this,←eq_sub_iff_add_eq',‹_ =(@ _) /@_›,Int.floor_eq_iff] at *zify[*]at*-- We will now show that `c = n*(l-⌊α⌋) + ⌊α⌋`.cases S5:lt_or_ge c (A * (l-.floor ↑x)+⌊x⌋ + 1)· simp_allhave:(c+1:ℝ)<=A*(l-⌊x⌋)+⌊x⌋+1:=by norm_castsimp_allcases this.eq_or_lt· /- For if `c = n*(l-⌊α⌋) + ⌊α⌋`, then```⌊(n+1)α⌋ = (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋)= (n+1)(n(l - ⌊α⌋) + ⌊α⌋) - n⌊α⌋ - n(n-1)(l-⌊α⌋)= 2n(l-⌊α⌋) + ⌊α⌋```as desired. -/repeat use by nlinarith/- Now, we show `c = n*(l-⌊α⌋) + ⌊α⌋` via contradictionsplit into two cases. First suppose `c ≤ n(l - ⌊α⌋) + ⌊α⌋ - 1`.```(n+1)α < (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋) + 1≤ (n+1)(n(l-⌊α⌋) + ⌊α⌋ - 1) - n⌊α⌋ - n(n-1)(l-⌊α⌋) + 1= 2n(l-⌊α⌋) + ⌊α⌋ - n= 2ln - 2n⌊α⌋ + ⌊α⌋ - n≤ (2α+⌊α⌋)n - 2n⌊α⌋ + ⌊α⌋ - n= nα + n(α-⌊α⌋-1) + ⌊α⌋n + α.```contradiction. -/nlinarith[(by norm_cast at* :(A*(l -⌊x⌋):ℝ)+⌊(x)⌋ >=(c)+01),9,Int.add_emod ↑5,Int.floor_le (@x : ℝ),Int.lt_floor_add_one (x:)]/- Next, suppose `c ≥ n(l - ⌊α⌋) + ⌊α⌋ + 1`.```(n+1)α ≥ (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋)≥ (n+1)(n(l-⌊α⌋) + ⌊α⌋ + 1) - n⌊α⌋ - n(n-1)(l-⌊α⌋)= 2n(l-⌊α⌋) + ⌊α⌋ + n + 1= 2ln - 2n⌊α⌋ + ⌊α⌋ + n + 1> (2α+⌊α⌋-1)n - 2n⌊α⌋ + ⌊α⌋ + n + 1= nα + n(α-⌊α⌋) + ⌊α⌋ + 1> n + α```contradiction. -/simp_allnlinarith[(by norm_cast:(c:ℝ)>=A*(l-⌊_⌋)+⌊_⌋+1),Int.floor_le x,Int.lt_floor_add_one x]rw [←Nat.cast_sum, mul_sub, Finset.sum_range_id]cases A with|_=>norm_num[mul_add]use Finset.sum_congr rfl <| by simp_all[add_comm,Int.floor_eq_iff]