zeta_3_irrational proof in Lean4

• Our paper can be found at here

• A blueprint can be found at here