AKS Formalisation in Lean

[metakunt]

Hey @tirix I have (with some help) formalised a result that we needed for AKS namely this one https://us.metamath.org/mpeuni/2ap1caineq.html

In lean it was quite easy to move forward, if you are interested here is the proof.

import Mathlib

open Nat

theorem inductiveineq2 (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1))*(x)!*(x+1)! <  (2*x + 1)! :=by
  induction' x, h1 using Nat.le_induction
  case base => decide
  case succ y ha hb =>
    have yh : y + 2 ≤ 2 * y + 3 := by linarith
    have hbd: 2*(y+1)*(y+2)≤ (2*y+2)*(2*y+3) := by exact Nat.mul_le_mul_left (2 * (y + 1)) yh
    have hoz : 0 < 2*(y+1)*(y+2) := by simp
    have opo : 1+1=2 := by exact rfl
    have aua : 2 * (y + 1) + 1 = 2*y+3 := by linarith
    have aue : (2 * y + 1 + 1)=2*y+2 :=by simp
    have aya : 2 ^ (y + 1) * y ! * (y + 1)! * (2 * (y + 1) * (y + 2)) =
    ( 2 ^ (y + 1)*2) * ( (y+1) *y ! ) *( (y + 2)* (y + 1)! ) :=by ring
    have aui : (2 * y + 1 + 2)=2*y+3 :=by simp
    have hh := Nat.mul_lt_mul_of_lt_of_le' hb hbd hoz
    conv =>
      lhs
      lhs
      lhs
      rw[pow_succ]
    conv =>
      lhs
      rhs
      congr
      rw[add_assoc]
      rhs
      rw[opo]
    conv =>
      rhs
      congr
      rw[aua]
    conv =>
      rhs
      rw[Nat.factorial_succ]
      rw[Nat.factorial_succ]
      rw[← mul_assoc]
      rw[mul_comm]
      rhs
      rw[mul_comm]
      rw[aue]
      rw[aui]
    conv at hh =>
      lhs
      rw[aya]
      rw[← Nat.factorial_succ]
      rhs
      rw[← Nat.factorial_succ]
      congr
      rw[add_assoc]
      rhs
      rw[opo]
    exact hh

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : 2^ (x+1) <  choose (2*x+1) x :=by
  have ho : (2*x+1)= (x+1)+x :=by ring
  have hoa : (x+1+x) =(2*x+1) := by ring
  have hua : (x+(x+1)) =(2*x+1) := by ring
  have hah := inductiveineq2 x h1
  rw[ho, add_choose, mul_comm]
  rw[mul_assoc] at hah
  have he := Nat.factorial_mul_factorial_dvd_factorial_add x (x+1)
  rw[hua] at he
  have hdn := Nat.lt_div_iff_mul_lt he (2^(x+1))
  conv at hdn =>
    rhs
    rw[mul_comm]
  have hodd := hdn.mpr hah
  rw[hoa]
  exact hodd

It's not that pretty but you could move a bit faster once you understood what was to prove. My idea was to formalise the statements in lean first and find a working proof there, and once we have formalised it it should be quite straightforward to prove it. Do you have any experience with lean? If so, we could tackle the argument of the algebraic closure of the Galois field and observe what arguments are necessary to prove it. Then once we have identified the arguments it should be quite easy to prove it.

What do you think?

[tirix]

That's pretty cool! I have never actually taken time to try out Lean, at most I've been browsing some pages and introduction, so unfortunately I'm in no way able to write new proofs in Lean, but I'm still interesting in having more Galois theory and theory of finite fields in Metamath!

[metakunt]

Yeah. Once my permutation results get merged I'd like to work a bit on Galois fields/algebraic closures.

My idea is to work backwards and assume the api as done. Then we could find the minimal set of theorems we need to have about Galois theory to prove at least some equations. After that we could figure out how to define Galois fields and prove some fundamental results.

I guess being in the algebraic closure of $\mathbb{F}_p$ it is easy to take arbitrary $r_0$-th roots, so I guess we need something like this. $\forall r \in \mathbb{N} \forall k < r \exists \mu \in \mathbb{F}_p : \mu^r = 1 \land \mu^k\neq 1 $

So that would be the existence of primitive roots. Could we try to formalise the statement of this one.

Also I am not sure how we want to do calculations in the closure of $\mathbb{F}_p$ Do we want to have formal elements in $\mathbb{Z}[X]$ and then "lift" them to the closure. I guess there are morphisms from each $\mathbb{F}_p^n$ to its algebraic closure, also there should be morphisms from $\mathbb{Z}[X]$ to $\mathbb{F}_p^n$ by taking the quotient modulo irreducible generator.

Also if you'd like to we could have occasional meetings over zoom or something equivalent to share ideas more rapidly.