This is the #Lean 4 #proof of the nonexistence of #God, based on "§2.4 Modeling English Propositions" p.37 of "A Logical Approach to Discrete Mathematics" by Gries and Schneider (1993):
• If God were able and willing to prevent evil, He would do so:
Able ∧ Willing → Prevents
• If God were unable to prevent evil, He would be impotent:
¬Able → Impotent
• If God were unwilling to prevent evil, He would be malevolent:
¬Willing → Malevolent
• God does not prevent evil:
¬Prevents
• If God exists, He is neither impotent nor malevolent:
GodExists → ¬Impotent ∧ ¬Malevolent
• Therefore, God does not exist:
¬GodExists
Shed no tears for me, were I to end up in #Hell. That my code type checks in Lean 4 at all is a little bit of #Heaven for me.