N_PEqualsNP.lean defines:
def P_equals_NP : Prop := True def SAT_in_P : Prop := True
So the theorem
theorem p_equals_np (n : ℕ) (hn : 5 ≤ n) : P_equals_NP
does not prove a formalized P = NP statement. It proves True.
N_PEqualsNP.lean defines:
def P_equals_NP : Prop := True def SAT_in_P : Prop := True
So the theorem
theorem p_equals_np (n : ℕ) (hn : 5 ≤ n) : P_equals_NP
does not prove a formalized P = NP statement. It proves True.